From 7a86aab6b034dafe36635178b277393cb5a2abb8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 22 Aug 2015 23:57:35 -0700 Subject: 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. --- Test/wishlist/exists-b-exists-not-b.dfy | 10 ++++++++++ Test/wishlist/exists-b-exists-not-b.dfy.expect | 8 ++++++++ 2 files changed, 18 insertions(+) create mode 100644 Test/wishlist/exists-b-exists-not-b.dfy create mode 100644 Test/wishlist/exists-b-exists-not-b.dfy.expect (limited to 'Test/wishlist') 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 -- cgit v1.2.3