From 0858e1e3e86a41d809ce17cf3a25e2289ccc3b8d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:13:21 -0700 Subject: Replace b || !b by true in Snapshots5.v1.dfy We can't prove `exists b: bool :: b || !b` when splitting is enabled, at least for now, and there's already a separate test for that particular issue in wishlist/ --- Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy index 05dbced0..7b207d74 100644 --- a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy @@ -17,9 +17,9 @@ method M() } else { - assert (exists b: bool :: b || !b) || 4 != 4; + assert (exists b: bool :: true) || 4 != 4; } - assert (exists b: bool :: b || !b) || 5 != 5; + assert (exists b: bool :: true) || 5 != 5; } -- cgit v1.2.3