summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-23 00:13:21 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-23 00:13:21 -0700
commit0858e1e3e86a41d809ce17cf3a25e2289ccc3b8d (patch)
treed393595d67f8f943cf51c83cd792c08f9a186eb1
parentdc08d67a27ffeb26889a56daa573ccc56daa1c0d (diff)
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/
-rw-r--r--Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy4
1 files changed, 2 insertions, 2 deletions
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;
}