From 6dfa82655aa7cb35bae6904e05887cdf960c6319 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 13 Jul 2015 11:55:06 -0700 Subject: Fix multiple tests that relied on z3 triggering on $Box Found by enabling auto-generated triggers and looking for failing tests --- Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy') diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy index c752bd38..f691384c 100644 --- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy +++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy @@ -117,6 +117,11 @@ class Tree { Repr := lft.Repr + {this} + rgt.Repr; } + lemma exists_intro(P: T -> bool, x: T) + requires P.requires(x) + requires P(x) + ensures exists y :: P.requires(y) && P(y) { } + method ComputeMax() returns (mx: int) requires Valid() && !IsEmpty(); ensures forall x :: x in Contents ==> x <= mx; @@ -124,13 +129,17 @@ class Tree { decreases Repr; { mx := value; + if (!left.IsEmpty()) { var m := left.ComputeMax(); mx := if mx < m then m else mx; } + if (!right.IsEmpty()) { var m := right.ComputeMax(); mx := if mx < m then m else mx; } + + exists_intro(x reads this => x in Contents && x == mx, mx); } } -- cgit v1.2.3