Add test for issue #2211

dafny-lang · Jun 15, 2023 · 8b349be · 8b349be
1 parent 8f1311c
commit 8b349be
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/Test/git-issues/git-issue-2211.dfy b/Test/git-issues/git-issue-2211.dfy
@@ -0,0 +1,16 @@
+// RUN: %exits-with 4 %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P1(a: int)
+predicate P2(a: int)
+
+predicate Q(s: seq<int>) {
+  forall i | 0 <= i < |s| ::
+    (P1(s[i]) || false) && (P2(s[i]) || false)  // Line 6
+}
+
+method M(s: seq<int>)
+  requires forall i | 0 <= i < |s| :: P1(s[i])
+  // requires forall i | 0 <= i < |s| :: P2(s[i])
+  ensures Q(s)
+{}
diff --git a/Test/git-issues/git-issue-2211.dfy.expect b/Test/git-issues/git-issue-2211.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