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

1 files changed, 20 insertions, 0 deletions

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);

+}