Add test for issue #4205

dafny-lang · Jun 22, 2023 · d316c50 · d316c50
1 parent 58b1b9b
commit d316c50
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/Test/git-issues/git-issue-4205.dfy b/Test/git-issues/git-issue-4205.dfy
@@ -0,0 +1,12 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait T {
+ opaque function bar(): int
+}
+
+class F extends T {
+ opaque function bar(): int {
+ 1
+ }
+}
diff --git a/Test/git-issues/git-issue-4205.dfy.expect b/Test/git-issues/git-issue-4205.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with TODO verified, TODO errors