Add test for issue #2402

dafny-lang · Nov 4, 2022 · 145754e · 145754e
1 parent 16cc15c
commit 145754e
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/Test/git-issues/git-issue-2402.dfy b/Test/git-issues/git-issue-2402.dfy
@@ -0,0 +1,16 @@
+// RUN: %dafny_0 /compile:1 /compileTarget:cs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module M 
+{ 
+    type T
+    const t : T
+    lemma Randomlemma()
+    {
+        forall i:int {}
+    }
+}
+
+module N refines M 
+{ 
+}
diff --git a/Test/git-issues/git-issue-2402.dfy.expect b/Test/git-issues/git-issue-2402.dfy.expect