From a2159cafdf6ae62f4199bd669103c68ddacf49f2 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Fri, 5 May 2023 16:37:00 -0700
Subject: [PATCH] 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>
---
 Test/git-issues/git-issue-2103.dfy        | 9 +++++++++
 Test/git-issues/git-issue-2103.dfy.expect | 1 +
 2 files changed, 10 insertions(+)
 create mode 100644 Test/git-issues/git-issue-2103.dfy
 create mode 100644 Test/git-issues/git-issue-2103.dfy.expect

diff --git a/Test/git-issues/git-issue-2103.dfy b/Test/git-issues/git-issue-2103.dfy
new file mode 100644
index 00000000000..9f807fd7a03
--- /dev/null
+++ 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
new file mode 100644
index 00000000000..00750edc07d
--- /dev/null
+++ b/Test/git-issues/git-issue-2103.dfy.expect
@@ -0,0 +1 @@
+3