Add tests for Issue 5521

Fixes dafny-lang#5521

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

@@ -0,0 +1,73 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s"
+
+module WithoutWitnessClause {
+  type Empty = x: int | false witness *
+
+  newtype NewEmpty = Empty // error: the default-witness 0 is not a witness
+
+  method OperateOnNewEmpty(x: NewEmpty)
+    ensures false
+  {
+    var y: Empty := x as Empty;
+  }
+
+  method Test() {
+    var x: NewEmpty := *;
+    OperateOnNewEmpty(x);
+    print 10 / 0;
+  }
+}
+
+module WithWitnessClause {
+  type Empty = x: int | false witness *
+
+  newtype NewEmpty = Empty witness 506 // error: 506 is not a witness
+
+  method OperateOnNewEmpty(x: NewEmpty)
+    ensures false
+  {
+    var y: Empty := x as Empty;
+  }
+
+  method Test() {
+    var x: NewEmpty := *;
+    OperateOnNewEmpty(x);
+    print 10 / 0;
+  }
+}
+
+module WithGhostWitnessClause {
+  type Empty = x: int | false witness *
+
+  newtype NewEmpty = Empty ghost witness 506 // error: 506 is not a ghost witness
+
+  method OperateOnNewEmpty(x: NewEmpty)
+    ensures false
+  {
+    var y: Empty := x as Empty;
+  }
+
+  method Test() {
+    var x: NewEmpty := *;
+    OperateOnNewEmpty(x); // error: x is used before it has really been initialized
+    print 10 / 0;
+  }
+}
+
+module DeclaredAsPossiblyEmpty {
+  type Empty = x: int | false witness *
+
+  newtype NewEmpty = Empty witness *
+
+  method OperateOnNewEmpty(x: NewEmpty)
+    ensures false
+  {
+    var y: Empty := x as Empty;
+  }
+
+  method Test() {
+    var x: NewEmpty := *;
+    OperateOnNewEmpty(x); // error: x is used before it has really been initialized
+    print 10 / 0;
+  }
+}

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

@@ -0,0 +1,7 @@
+git-issue-5521.dfy(6,10): Error: trying witness 0: result of operation might violate subset type constraint for 'Empty'
+git-issue-5521.dfy(24,35): Error: result of operation might violate subset type constraint for 'Empty'
+git-issue-5521.dfy(42,41): Error: result of operation might violate subset type constraint for 'Empty'
+git-issue-5521.dfy(52,22): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here
+git-issue-5521.dfy(70,22): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here
+
+Dafny program verifier finished with 6 verified, 5 errors