Add test cases

Test/git-issues/git-issue-3883.dfy

@@ -0,0 +1,54 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+type MyType<T> = x: T | true witness *
+type MyInt<T> = x: int | true witness *
+
+method Main() {
+ var a: MyType<int> := 13; // NOTE: this used to not verify
+ TestMyTest(a, 14); // 13 14 // NOTE: this used to crash the resolved
+ var b: MyType<bool> := true;
+ TestMyTest(b, false); // true false
+ print a, " ", b, "\n"; // 13 true
+
+ var c: MyInt<object> := 18;
+ var d: MyInt<bv19> := 19;
+ print c, " ", d, "\n"; // 18 19
+
+ TestOthers();
+
+ DoIt<real>();
+}
+
+method TestMyTest<U>(m: MyType<U>, u: U) {
+ var w: U := u;
+ var n: MyType<U> := m;
+ w := m;
+ n := u;
+ print m, " ", u, "\n";
+}
+
+datatype ABC<X> = MakeABC(X)
+datatype XYZ<A(0)> = MakeXYZ(A)
+type SSS<Y> = s: seq<Y> | |s| <= 10
+
+method TestOthers() {
+ var a := MakeABC(10);
+ var b := MakeXYZ(null);
+ var c: SSS<bool> := [false, true, false];
+ print a, " ", b, " ", c, "\n"; // 10 null [false, true, false]
+}
+
+type ST0<T, U(0)> = x: int | x % 5 == 0
+type ST1<T, U(0)> = x: int | (if var m: map<T,U> := map[]; m == map[] then 0 else 8) <= x
+
+method DoIt<X(0)>() {
+ var t0: ST0<int, X>;
+ var t1: ST1<int, X>;
+ Print(t0, " "); // 0-0
+ Print(t1, "\n"); // 0-0
+}
+
+method Print<X(0)>(x: X, suffix: string) {
+ var y: X;
+ print x, "-", y, suffix;
+}

Test/git-issues/git-issue-3883.dfy.expect

@@ -0,0 +1,6 @@
+13 14
+true false
+13 true
+18 19
+10 null [false, true, false]
+0-0 0-0