diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-13 11:55:06 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-13 11:55:06 -0700 |
commit | 6dfa82655aa7cb35bae6904e05887cdf960c6319 (patch) | |
tree | fcc960db0cce120eccce3fb4be52edf9ff9325c3 /Test/dafny4/GHC-MergeSort.dfy | |
parent | 64495ae998749da057b3a717aba6ef53a3e8006e (diff) |
Fix multiple tests that relied on z3 triggering on $Box
Found by enabling auto-generated triggers and looking for failing tests
Diffstat (limited to 'Test/dafny4/GHC-MergeSort.dfy')
-rw-r--r-- | Test/dafny4/GHC-MergeSort.dfy | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy index e06773eb..976b8a27 100644 --- a/Test/dafny4/GHC-MergeSort.dfy +++ b/Test/dafny4/GHC-MergeSort.dfy @@ -412,11 +412,8 @@ lemma sorted_replaceSuffix(xs: List<G>, ys: List<G>, zs: List<G>) match xs {
case Nil =>
case Cons(c, xs') =>
- forall a,b | a in multiset_of(xs') && b in multiset_of(Cons(c, zs))
- ensures Below(a, b);
- {
- sorted_reverse(xs', Cons(c, ys));
- }
+ sorted_reverse(xs, ys);
+ sorted_reverse(xs', Cons(c, ys));
sorted_replaceSuffix(xs', Cons(c, ys), Cons(c, zs));
}
}
|