diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-23 00:13:21 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-23 00:13:21 -0700 |
| commit | 0858e1e3e86a41d809ce17cf3a25e2289ccc3b8d (patch) | |
| tree | d393595d67f8f943cf51c83cd792c08f9a186eb1 | |
| parent | dc08d67a27ffeb26889a56daa573ccc56daa1c0d (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.dfy | 4 |
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;
}
|