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.expect | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 Test/wishlist/exists-b-exists-not-b.dfy.expect (limited to 'Test/wishlist/exists-b-exists-not-b.dfy.expect') 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