Add tests for previously fixed bug (#3959)

Closes #2103 Issue #2103 was fixed as part of PR #3893. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · May 5, 2023 · a2159ca · a2159ca
1 parent d3d6087
commit a2159ca
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/Test/git-issues/git-issue-2103.dfy b/Test/git-issues/git-issue-2103.dfy
@@ -0,0 +1,9 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+datatype DT_<+A> = DT(ret: A)
+type DT<A> = r: DT_<A> | true witness *
+
+method Main() {
+ var d := DT(3);
+ print d, "\n"; // 3
+}
diff --git a/Test/git-issues/git-issue-2103.dfy.expect b/Test/git-issues/git-issue-2103.dfy.expect
@@ -0,0 +1 @@
+3