diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-22 23:57:35 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-22 23:57:35 -0700 |
| commit | 7a86aab6b034dafe36635178b277393cb5a2abb8 (patch) | |
| tree | 81fd3a3ce47afc08505fc975237a4fccaf89ce98 | |
| parent | 2142e51d713394d384b0f33c1189f633dcbe301a (diff) | |
Add one more wish: it would be nice to be able to prove exists b: bool :: b
This is an issue because splitting `exists b: bool :: b || !b` produces two
quantifiers that we don't know how to prove.
| -rw-r--r-- | Test/wishlist/exists-b-exists-not-b.dfy | 10 | ||||
| -rw-r--r-- | Test/wishlist/exists-b-exists-not-b.dfy.expect | 8 |
2 files changed, 18 insertions, 0 deletions
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy b/Test/wishlist/exists-b-exists-not-b.dfy new file mode 100644 index 00000000..711c5611 --- /dev/null +++ b/Test/wishlist/exists-b-exists-not-b.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// It would be great if Dafny was able to verify the following statements;
+// otherwise, trigger splitting prevents `exists b :: b || not b` from verifying
+
+method M() {
+ assert exists b: bool :: b; // WISH
+ assert exists b: bool :: !b; // WISH
+}
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy.expect b/Test/wishlist/exists-b-exists-not-b.dfy.expect new file mode 100644 index 00000000..c785ee97 --- /dev/null +++ b/Test/wishlist/exists-b-exists-not-b.dfy.expect @@ -0,0 +1,8 @@ +exists-b-exists-not-b.dfy(8,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+exists-b-exists-not-b.dfy(9,9): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 1 verified, 2 errors
|