Add test for issue #4315

dafny-lang · Jul 20, 2023 · 7d37370 · 7d37370
1 parent 2901f18
commit 7d37370
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/Test/git-issues/git-issue-4315.dfy b/Test/git-issues/git-issue-4315.dfy
@@ -0,0 +1,11 @@
+// RUN: %baredafny run %args -t:cs "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M1 {
+  class C {
+    opaque function f() : bool { true }
+  }
+}
+
+module M2 refines M1 {
+}
diff --git a/Test/git-issues/git-issue-4315.dfy.expect b/Test/git-issues/git-issue-4315.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with TODO verified, TODO errors
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@

		Dafny program verifier finished with TODO verified, TODO errors