Add a test that shows an empty datatype is provably empty

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy

@@ -19,3 +19,13 @@ module NoAutoInit {
  }
  }
 }
+
+module ProvablyEmpty {
+ datatype BadList<X> = Cons(head: X, tail: BadList<X>) // warning: no instances
+
+ lemma NeverGetHere<X>(xs: BadList<X>)
+ ensures false
+ {
+ NeverGetHere(xs.tail);
+ }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy.expect

@@ -1,4 +1,5 @@
+git-issue-4939b.dfy(24,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'BadList' can be constructed
 git-issue-4939b.dfy(16,12): Error: variable 'a', which is subject to definite-assignment rules, might be uninitialized here
 git-issue-4939b.dfy(18,12): Error: variable 'b', which is subject to definite-assignment rules, might be uninitialized here
 
-Dafny program verifier finished with 0 verified, 2 errors
+Dafny program verifier finished with 1 verified, 2 errors