Fixed bug where free conditions preceded checked conditions (for inlined predicates)

2 files changed, 25 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 13613f66..88cad7fa 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1419,8 +1419,12 @@ EqualityTypes.dfy(115,16): Error: == can only be applied to expressions of types
 11 resolution/type errors detected in EqualityTypes.dfy

 

 -------------------- SplitExpr.dfy --------------------

+SplitExpr.dfy(89,15): Error: loop invariant violation

+SplitExpr.dfy(83,44): Related location

+Execution trace:

+    SplitExpr.dfy(88,3): anon7_LoopHead

 

-Dafny program verifier finished with 8 verified, 0 errors

+Dafny program verifier finished with 10 verified, 1 error

 

 -------------------- LoopModifies.dfy --------------------

 LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause

diff --git a/Test/dafny0/SplitExpr.dfy b/Test/dafny0/SplitExpr.dfy
index 3e67db58..12d0ae55 100644
--- a/Test/dafny0/SplitExpr.dfy
+++ b/Test/dafny0/SplitExpr.dfy
@@ -73,3 +73,23 @@ method M(N: nat)
     i := i + 1;

   }

 }

+

+// ----- orderings of checked vs. free  -----

+// The translation must always put checked things before free things.  In most situations,

+// this does not actually matter, but it does matter for loop invariants of loops that have

+// no backedges (that is, loops where Boogie's simple dead-code analysis figures prunes

+// away the backedges.

+

+predicate AnyPredicate(a: int, b: int) { a <= b }

+

+method NoLoop(N: nat)

+{

+  var i;

+  while i < N

+    invariant AnyPredicate(i, N);  // error: may not hold initially

+  {

+    i := i + 1;

+    break;  // this makes the loop not a loop

+  }

+  assert AnyPredicate(i, N);

+}