More and improved CaptureState info

2 files changed, 251 insertions, 201 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4080129b..e6e0a7dd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2452,6 +2452,11 @@ namespace Microsoft.Dafny {
           }

           builder.Add(new Bpl.HavocCmd(m.tok, outH));

         }

+        // mark the end of the modifles/out-parameter havocking with a CaptureState; make its location be the first ensures clause, if any (and just

+        // omit the CaptureState if there's no ensures clause)

+        if (m.Ens.Count != 0) {

+          builder.Add(CaptureState(m.Ens[0].E.tok, "post-state"));

+        }

 

         // check wellformedness of postconditions

         foreach (MaybeFreeExpression p in m.Ens) {

@@ -2605,6 +2610,7 @@ namespace Microsoft.Dafny {
 

       // set up the information used to verify the method's modifies clause

       DefineFrame(m.tok, m.Mod.Expressions, builder, localVariables, null);

+      builder.Add(CaptureState(m.tok, "initial state"));

     }

 

     void GenerateIteratorImplPrelude(IteratorDecl iter, List<Variable> inParams, List<Variable> outParams,

@@ -2623,6 +2629,7 @@ namespace Microsoft.Dafny {
       iteratorFrame.Add(new FrameExpression(iter.tok, th, null));

       iteratorFrame.AddRange(iter.Modifies.Expressions);

       DefineFrame(iter.tok, iteratorFrame, builder, localVariables, null);

+      builder.Add(CaptureState(iter.tok, "initial state"));

     }

 

     Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {

@@ -2648,7 +2655,7 @@ namespace Microsoft.Dafny {
 

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);

       // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool

-      Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type of the $_Frame variable

+      Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type and name of the $_Frame variable

       Contract.Assert(theFrame.Type != null);  // follows from the postcondition of TheFrame

       Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? theFrame.Name, theFrame.Type));

       localVariables.Add(frame);

@@ -2664,10 +2671,6 @@ namespace Microsoft.Dafny {
                                            Bpl.Expr.Imp(ante, consequent));

 

       builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));

-      if (name == null) {

-        // put a CaptureState here, so that there will be at least one CaptureState for the procedure

-        builder.Add(CaptureState(tok, "initial state"));

-      }

     }

 

     void CheckFrameSubset(IToken tok, List<FrameExpression/*!*/>/*!*/ calleeFrame,

@@ -2994,9 +2997,10 @@ namespace Microsoft.Dafny {
         InsertChecksum(f, proc, true);

       }

 

-      List<Variable> implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

-      List<Variable> locals = new List<Variable>();

-      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      var implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

+      var locals = new List<Variable>();

+      var builder = new Bpl.StmtListBuilder();

+      builder.Add(CaptureState(f.tok, "initial state"));

 

       // check well-formedness of the preconditions (including termination, but no reads checks), and then

       // assume each one of them

@@ -3798,9 +3802,10 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < e.Vars.Count; i++) {

             var vr = e.Vars[i];

             var tp = TrType(vr.Type);

-            var v = new Bpl.LocalVariable(vr.tok, new Bpl.TypedIdent(vr.tok, vr.AssignUniqueName(currentDeclaration), tp));

+            var nm = vr.AssignUniqueName(currentDeclaration);

+            var v = new Bpl.LocalVariable(vr.tok, new Bpl.TypedIdent(vr.tok, nm, tp));

             locals.Add(v);

-            var lhs = new Bpl.IdentifierExpr(vr.tok, vr.AssignUniqueName(currentDeclaration), tp);

+            var lhs = new Bpl.IdentifierExpr(vr.tok, nm, tp);

 

             CheckWellformedWithResult(e.RHSs[i], options, lhs, vr.Type, locals, builder, etran);

             substMap.Add(vr, new BoogieWrapper(lhs, vr.Type));

@@ -6321,6 +6326,7 @@ namespace Microsoft.Dafny {
       }

 

       Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();

+      loopBodyBuilder.Add(CaptureState(s.Tok, "after some loop iterations"));

       // as the first thing inside the loop, generate:  if (!w) { CheckWellformed(inv); assume false; }

       invDefinednessBuilder.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

       loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(s.Tok), null, null));

@@ -6334,7 +6340,6 @@ namespace Microsoft.Dafny {
       guardBreak.Add(new Bpl.BreakCmd(s.Tok, null));

       loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, guard, guardBreak.Collect(s.Tok), null, null));

 

-      loopBodyBuilder.Add(CaptureState(s.Tok, "loop entered"));

       // termination checking

       if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {

         // omit termination checking for this loop

@@ -6372,7 +6377,6 @@ namespace Microsoft.Dafny {
       Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok);

 

       builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, body));

-      builder.Add(CaptureState(s.Tok, "loop exit"));

     }

 

     void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index eec55394..c21ddbc8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -122,11 +122,13 @@ Execution trace:
     (0,0): anon3_Then

 NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative

 Execution trace:

+    (0,0): anon0

     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

 NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Then

 

 Dafny program verifier finished with 15 verified, 9 errors

@@ -134,6 +136,7 @@ Dafny program verifier finished with 15 verified, 9 errors
 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 Definedness.dfy(15,16): Error: possible division by zero

 Execution trace:

@@ -201,88 +204,88 @@ Execution trace:
     (0,0): anon0

 Definedness.dfy(105,15): Error: possible division by zero

 Execution trace:

-    Definedness.dfy(105,5): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    Definedness.dfy(105,5): anon9_Else

+    Definedness.dfy(105,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    Definedness.dfy(105,5): anon8_Else

 Definedness.dfy(114,23): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(113,5): anon13_LoopHead

-    (0,0): anon13_LoopBody

-    (0,0): anon14_Then

+    Definedness.dfy(113,5): anon12_LoopHead

+    (0,0): anon12_LoopBody

+    (0,0): anon13_Then

 Definedness.dfy(120,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(113,5): anon13_LoopHead

-    (0,0): anon13_LoopBody

-    Definedness.dfy(113,5): anon14_Else

-    (0,0): anon15_Then

-    Definedness.dfy(119,5): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    (0,0): anon17_Then

+    Definedness.dfy(113,5): anon12_LoopHead

+    (0,0): anon12_LoopBody

+    Definedness.dfy(113,5): anon13_Else

+    (0,0): anon14_Then

+    Definedness.dfy(119,5): anon15_LoopHead

+    (0,0): anon15_LoopBody

+    (0,0): anon16_Then

 Definedness.dfy(130,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(129,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    (0,0): anon8_Then

+    Definedness.dfy(129,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

 Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

 Definedness.dfy(131,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(129,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    (0,0): anon8_Then

+    Definedness.dfy(129,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

 Definedness.dfy(140,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(140,5): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    Definedness.dfy(140,5): anon10_Else

+    Definedness.dfy(140,5): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    Definedness.dfy(140,5): anon9_Else

 Definedness.dfy(159,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(153,5): anon17_LoopHead

-    (0,0): anon17_LoopBody

-    Definedness.dfy(153,5): anon18_Else

-    (0,0): anon19_Then

+    Definedness.dfy(153,5): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    Definedness.dfy(153,5): anon17_Else

+    (0,0): anon18_Then

     (0,0): anon5

-    (0,0): anon20_Then

-    Definedness.dfy(159,5): anon21_LoopHead

-    (0,0): anon21_LoopBody

-    Definedness.dfy(159,5): anon22_Else

+    (0,0): anon19_Then

+    Definedness.dfy(159,5): anon20_LoopHead

+    (0,0): anon20_LoopBody

+    Definedness.dfy(159,5): anon21_Else

 Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

 Definedness.dfy(178,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(170,5): anon19_LoopHead

-    (0,0): anon19_LoopBody

-    Definedness.dfy(170,5): anon20_Else

-    (0,0): anon21_Then

-    Definedness.dfy(177,5): anon22_LoopHead

-    (0,0): anon22_LoopBody

+    Definedness.dfy(170,5): anon18_LoopHead

+    (0,0): anon18_LoopBody

+    Definedness.dfy(170,5): anon19_Else

+    (0,0): anon20_Then

+    Definedness.dfy(177,5): anon21_LoopHead

+    (0,0): anon21_LoopBody

+    (0,0): anon22_Then

     (0,0): anon23_Then

-    (0,0): anon24_Then

     (0,0): anon11

 Definedness.dfy(193,19): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(191,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    (0,0): anon8_Then

+    Definedness.dfy(191,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

 Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

 Definedness.dfy(193,28): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(191,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    (0,0): anon8_Then

+    Definedness.dfy(191,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

 Definedness.dfy(212,10): Error BP5003: A postcondition might not hold on this return path.

 Definedness.dfy(214,46): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -290,12 +293,14 @@ Execution trace:
     (0,0): anon5_Else

 Definedness.dfy(221,22): Error: target object may be null

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

 Definedness.dfy(234,10): Error BP5003: A postcondition might not hold on this return path.

 Definedness.dfy(237,24): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon7_Then

     (0,0): anon2

     (0,0): anon8_Else

@@ -306,6 +311,7 @@ Dafny program verifier finished with 21 verified, 37 errors
 FunctionSpecifications.dfy(32,25): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(28,13): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon8_Else

     (0,0): anon9_Else

     (0,0): anon10_Then

@@ -313,6 +319,7 @@ Execution trace:
 FunctionSpecifications.dfy(42,3): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(37,24): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon11_Else

     (0,0): anon14_Else

     (0,0): anon15_Then

@@ -324,6 +331,7 @@ Execution trace:
 FunctionSpecifications.dfy(56,10): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(57,22): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

 

 Dafny program verifier finished with 8 verified, 4 errors

@@ -477,35 +485,41 @@ Execution trace:
     (0,0): anon11

 Array.dfy(117,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

+    (0,0): anon0

     (0,0): anon9_Else

     (0,0): anon10_Then

     (0,0): anon11_Then

     (0,0): anon12_Then

 Array.dfy(119,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

+    (0,0): anon0

     (0,0): anon9_Else

     (0,0): anon10_Then

     (0,0): anon11_Then

     (0,0): anon12_Else

 Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

+    (0,0): anon0

     (0,0): anon9_Else

     (0,0): anon10_Then

     (0,0): anon11_Then

     (0,0): anon12_Else

 Array.dfy(121,8): Error: insufficient reads clause to read the indicated range of array elements

 Execution trace:

+    (0,0): anon0

     (0,0): anon9_Else

     (0,0): anon10_Then

     (0,0): anon11_Then

     (0,0): anon12_Else

 Array.dfy(147,6): Error: insufficient reads clause to read array element

 Execution trace:

+    (0,0): anon0

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

 Array.dfy(155,6): Error: insufficient reads clause to read array element

 Execution trace:

+    (0,0): anon0

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

@@ -656,6 +670,7 @@ Modules2.dfy(50,11): Error: The name f ambiguously refers to a static member in
 -------------------- BadFunction.dfy --------------------

 BadFunction.dfy(6,3): Error: failure to decrease termination measure

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 

 Dafny program verifier finished with 2 verified, 1 error

@@ -768,6 +783,7 @@ Execution trace:
     (0,0): anon10_Then

 ControlStructures.dfy(51,3): Error: missing case in case statement: Red

 Execution trace:

+    (0,0): anon0

     (0,0): anon8_Else

     (0,0): anon9_Else

     (0,0): anon10_Else

@@ -780,89 +796,89 @@ Execution trace:
 ControlStructures.dfy(215,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(194,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon59_LoopHead

+    (0,0): anon59_LoopBody

+    ControlStructures.dfy(194,3): anon60_Else

+    ControlStructures.dfy(194,3): anon61_Else

+    ControlStructures.dfy(198,5): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(194,3): anon63_Else

-    ControlStructures.dfy(194,3): anon64_Else

-    ControlStructures.dfy(198,5): anon65_LoopHead

-    (0,0): anon65_LoopBody

-    ControlStructures.dfy(198,5): anon66_Else

-    ControlStructures.dfy(198,5): anon67_Else

+    ControlStructures.dfy(198,5): anon63_Else

+    ControlStructures.dfy(198,5): anon64_Else

+    (0,0): anon68_Then

+    ControlStructures.dfy(210,9): anon69_LoopHead

+    (0,0): anon69_LoopBody

+    ControlStructures.dfy(210,9): anon70_Else

     (0,0): anon71_Then

-    ControlStructures.dfy(210,9): anon72_LoopHead

-    (0,0): anon72_LoopBody

-    ControlStructures.dfy(210,9): anon73_Else

-    (0,0): anon74_Then

 ControlStructures.dfy(232,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(194,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon59_LoopHead

+    (0,0): anon59_LoopBody

+    ControlStructures.dfy(194,3): anon60_Else

+    ControlStructures.dfy(194,3): anon61_Else

+    ControlStructures.dfy(198,5): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(194,3): anon63_Else

-    ControlStructures.dfy(194,3): anon64_Else

-    ControlStructures.dfy(198,5): anon65_LoopHead

-    (0,0): anon65_LoopBody

-    ControlStructures.dfy(198,5): anon66_Else

-    ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon71_Then

-    ControlStructures.dfy(210,9): anon72_LoopHead

-    (0,0): anon72_LoopBody

-    ControlStructures.dfy(210,9): anon73_Else

-    ControlStructures.dfy(210,9): anon74_Else

-    (0,0): anon75_Then

+    ControlStructures.dfy(198,5): anon63_Else

+    ControlStructures.dfy(198,5): anon64_Else

+    (0,0): anon68_Then

+    ControlStructures.dfy(210,9): anon69_LoopHead

+    (0,0): anon69_LoopBody

+    ControlStructures.dfy(210,9): anon70_Else

+    ControlStructures.dfy(210,9): anon71_Else

+    (0,0): anon72_Then

     (0,0): after_4

-    ControlStructures.dfy(221,7): anon77_LoopHead

-    (0,0): anon77_LoopBody

-    ControlStructures.dfy(221,7): anon78_Else

-    ControlStructures.dfy(221,7): anon79_Else

-    (0,0): anon81_Then

+    ControlStructures.dfy(221,7): anon74_LoopHead

+    (0,0): anon74_LoopBody

+    ControlStructures.dfy(221,7): anon75_Else

+    ControlStructures.dfy(221,7): anon76_Else

+    (0,0): anon78_Then

     (0,0): anon38

     (0,0): after_9

-    (0,0): anon86_Then

-    (0,0): anon53

+    (0,0): anon83_Then

+    (0,0): anon52

 ControlStructures.dfy(235,30): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(194,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon59_LoopHead

+    (0,0): anon59_LoopBody

+    ControlStructures.dfy(194,3): anon60_Else

+    ControlStructures.dfy(194,3): anon61_Else

+    ControlStructures.dfy(198,5): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(194,3): anon63_Else

-    ControlStructures.dfy(194,3): anon64_Else

-    ControlStructures.dfy(198,5): anon65_LoopHead

-    (0,0): anon65_LoopBody

-    ControlStructures.dfy(198,5): anon66_Else

-    ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon68_Then

+    ControlStructures.dfy(198,5): anon63_Else

+    ControlStructures.dfy(198,5): anon64_Else

+    (0,0): anon65_Then

     (0,0): after_5

-    (0,0): anon87_Then

-    (0,0): anon88_Then

-    (0,0): anon58

+    (0,0): anon84_Then

+    (0,0): anon85_Then

+    (0,0): anon56

 ControlStructures.dfy(238,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(194,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon59_LoopHead

+    (0,0): anon59_LoopBody

+    ControlStructures.dfy(194,3): anon60_Else

+    ControlStructures.dfy(194,3): anon61_Else

+    ControlStructures.dfy(198,5): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(194,3): anon63_Else

-    ControlStructures.dfy(194,3): anon64_Else

-    ControlStructures.dfy(198,5): anon65_LoopHead

-    (0,0): anon65_LoopBody

-    ControlStructures.dfy(198,5): anon66_Else

-    ControlStructures.dfy(198,5): anon67_Else

-    (0,0): anon71_Then

-    ControlStructures.dfy(210,9): anon72_LoopHead

-    (0,0): anon72_LoopBody

-    ControlStructures.dfy(210,9): anon73_Else

-    ControlStructures.dfy(210,9): anon74_Else

-    (0,0): anon75_Then

+    ControlStructures.dfy(198,5): anon63_Else

+    ControlStructures.dfy(198,5): anon64_Else

+    (0,0): anon68_Then

+    ControlStructures.dfy(210,9): anon69_LoopHead

+    (0,0): anon69_LoopBody

+    ControlStructures.dfy(210,9): anon70_Else

+    ControlStructures.dfy(210,9): anon71_Else

+    (0,0): anon72_Then

     (0,0): after_4

-    ControlStructures.dfy(221,7): anon77_LoopHead

-    (0,0): anon77_LoopBody

-    ControlStructures.dfy(221,7): anon78_Else

-    ControlStructures.dfy(221,7): anon79_Else

+    ControlStructures.dfy(221,7): anon74_LoopHead

+    (0,0): anon74_LoopBody

+    ControlStructures.dfy(221,7): anon75_Else

+    ControlStructures.dfy(221,7): anon76_Else

+    (0,0): anon79_Then

     (0,0): anon82_Then

-    (0,0): anon85_Then

     (0,0): after_8

-    (0,0): anon89_Then

-    (0,0): anon61

+    (0,0): anon86_Then

+    (0,0): anon58

 

 Dafny program verifier finished with 22 verified, 10 errors

 

@@ -876,49 +892,50 @@ Execution trace:
 Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(105,3): anon7_LoopHead

-    (0,0): anon7_LoopBody

+    Termination.dfy(105,3): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    Termination.dfy(105,3): anon7_Else

     Termination.dfy(105,3): anon8_Else

-    Termination.dfy(105,3): anon9_Else

 Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(113,3): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    Termination.dfy(113,3): anon10_Else

-    (0,0): anon11_Then

+    Termination.dfy(113,3): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    Termination.dfy(113,3): anon9_Else

+    (0,0): anon10_Then

     (0,0): anon5

-    Termination.dfy(113,3): anon12_Else

+    Termination.dfy(113,3): anon11_Else

 Termination.dfy(122,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(122,3): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    Termination.dfy(122,3): anon10_Else

-    (0,0): anon11_Then

+    Termination.dfy(122,3): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    Termination.dfy(122,3): anon9_Else

+    (0,0): anon10_Then

     (0,0): anon5

-    Termination.dfy(122,3): anon12_Else

+    Termination.dfy(122,3): anon11_Else

 Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

 Execution trace:

     (0,0): anon0

-    Termination.dfy(122,3): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    Termination.dfy(122,3): anon10_Else

-    (0,0): anon11_Then

+    Termination.dfy(122,3): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    Termination.dfy(122,3): anon9_Else

+    (0,0): anon10_Then

     (0,0): anon5

-    Termination.dfy(122,3): anon12_Else

+    Termination.dfy(122,3): anon11_Else

 Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

 Termination.dfy(291,3): Error: decreases expression might not decrease

 Execution trace:

-    Termination.dfy(291,3): anon10_LoopHead

-    (0,0): anon10_LoopBody

+    Termination.dfy(291,3): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    Termination.dfy(291,3): anon10_Else

     Termination.dfy(291,3): anon11_Else

-    Termination.dfy(291,3): anon12_Else

-    (0,0): anon13_Else

+    (0,0): anon12_Else

 

 Dafny program verifier finished with 59 verified, 7 errors

 

@@ -1088,14 +1105,14 @@ TypeParameters.dfy(175,15): Error BP5005: This loop invariant might not be maint
 TypeParameters.dfy(175,38): Related location

 Execution trace:

     (0,0): anon0

-    TypeParameters.dfy(168,3): anon17_LoopHead

-    (0,0): anon17_LoopBody

-    TypeParameters.dfy(168,3): anon18_Else

-    (0,0): anon20_Then

-    TypeParameters.dfy(174,3): anon21_LoopHead

-    (0,0): anon21_LoopBody

-    TypeParameters.dfy(174,3): anon22_Else

-    TypeParameters.dfy(174,3): anon24_Else

+    TypeParameters.dfy(168,3): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    TypeParameters.dfy(168,3): anon17_Else

+    (0,0): anon19_Then

+    TypeParameters.dfy(174,3): anon20_LoopHead

+    (0,0): anon20_LoopBody

+    TypeParameters.dfy(174,3): anon21_Else

+    TypeParameters.dfy(174,3): anon23_Else

 

 Dafny program verifier finished with 50 verified, 8 errors

 

@@ -1147,22 +1164,28 @@ Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in
 -------------------- Corecursion.dfy --------------------

 Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 Corecursion.dfy(21,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 Corecursion.dfy(56,5): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 Corecursion.dfy(69,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

 Corecursion.dfy(91,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

 Corecursion.dfy(101,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts)

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

 

@@ -1342,17 +1365,17 @@ Execution trace:
 LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-    LoopModifies.dfy(14,4): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    LoopModifies.dfy(14,4): anon10_Else

-    LoopModifies.dfy(14,4): anon12_Else

+    LoopModifies.dfy(14,4): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    LoopModifies.dfy(14,4): anon9_Else

+    LoopModifies.dfy(14,4): anon11_Else

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

 Execution trace:

     (0,0): anon0

-    LoopModifies.dfy(42,4): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    LoopModifies.dfy(42,4): anon10_Else

-    LoopModifies.dfy(42,4): anon12_Else

+    LoopModifies.dfy(42,4): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    LoopModifies.dfy(42,4): anon9_Else

+    LoopModifies.dfy(42,4): anon11_Else

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

 Execution trace:

     (0,0): anon0

@@ -1366,10 +1389,10 @@ Execution trace:
 LoopModifies.dfy(98,8): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-    LoopModifies.dfy(90,4): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    LoopModifies.dfy(90,4): anon10_Else

-    LoopModifies.dfy(90,4): anon12_Else

+    LoopModifies.dfy(90,4): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    LoopModifies.dfy(90,4): anon9_Else

+    LoopModifies.dfy(90,4): anon11_Else

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

 Execution trace:

     (0,0): anon0

@@ -1384,21 +1407,21 @@ Execution trace:
 LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-    LoopModifies.dfy(193,4): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    LoopModifies.dfy(193,4): anon10_Else

-    LoopModifies.dfy(193,4): anon12_Else

+    LoopModifies.dfy(193,4): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    LoopModifies.dfy(193,4): anon9_Else

+    LoopModifies.dfy(193,4): anon11_Else

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

 Execution trace:

     (0,0): anon0

-    LoopModifies.dfy(273,4): anon17_LoopHead

-    (0,0): anon17_LoopBody

-    LoopModifies.dfy(273,4): anon18_Else

-    LoopModifies.dfy(273,4): anon20_Else

-    LoopModifies.dfy(281,7): anon21_LoopHead

-    (0,0): anon21_LoopBody

-    LoopModifies.dfy(281,7): anon22_Else

-    LoopModifies.dfy(281,7): anon24_Else

+    LoopModifies.dfy(273,4): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    LoopModifies.dfy(273,4): anon17_Else

+    LoopModifies.dfy(273,4): anon19_Else

+    LoopModifies.dfy(281,7): anon20_LoopHead

+    (0,0): anon20_LoopBody

+    LoopModifies.dfy(281,7): anon21_Else

+    LoopModifies.dfy(281,7): anon23_Else

 

 Dafny program verifier finished with 23 verified, 9 errors

 

@@ -1420,6 +1443,7 @@ Execution trace:
 Refinement.dfy(90,12): Error BP5003: A postcondition might not hold on this return path.

 Refinement.dfy(69,15): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this return path.

 Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.

@@ -1504,9 +1528,11 @@ Dafny program verifier finished with 54 verified, 4 errors
 -------------------- PredExpr.dfy --------------------

 PredExpr.dfy(4,12): Error: condition in assert expression might not hold

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Else

 PredExpr.dfy(49,17): Error: condition in assert expression might not hold

@@ -1556,12 +1582,12 @@ Skeletons.dfy(42,3): Error BP5003: A postcondition might not hold on this return
 Skeletons.dfy(41,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    Skeletons.dfy[C0](29,5): anon12_LoopHead

-    (0,0): anon12_LoopBody

-    Skeletons.dfy[C0](29,5): anon13_Else

-    (0,0): anon14_Then

-    Skeletons.dfy[C0](34,19): anon16_Else

-    (0,0): anon11

+    Skeletons.dfy[C0](29,5): anon11_LoopHead

+    (0,0): anon11_LoopBody

+    Skeletons.dfy[C0](29,5): anon12_Else

+    (0,0): anon13_Then

+    Skeletons.dfy[C0](34,19): anon15_Else

+    (0,0): anon10

 

 Dafny program verifier finished with 9 verified, 1 error

 

@@ -1727,28 +1753,28 @@ Execution trace:
 Iterators.dfy(205,7): Error: an assignment to _new is only allowed to shrink the set

 Execution trace:

     (0,0): anon0

-    Iterators.dfy(194,3): anon17_LoopHead

-    (0,0): anon17_LoopBody

-    Iterators.dfy(194,3): anon18_Else

-    Iterators.dfy(194,3): anon20_Else

-    (0,0): anon21_Then

+    Iterators.dfy(194,3): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    Iterators.dfy(194,3): anon17_Else

+    Iterators.dfy(194,3): anon19_Else

+    (0,0): anon20_Then

 Iterators.dfy(209,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Iterators.dfy(194,3): anon17_LoopHead

-    (0,0): anon17_LoopBody

-    Iterators.dfy(194,3): anon18_Else

-    Iterators.dfy(194,3): anon20_Else

-    (0,0): anon22_Then

+    Iterators.dfy(194,3): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    Iterators.dfy(194,3): anon17_Else

+    Iterators.dfy(194,3): anon19_Else

+    (0,0): anon21_Then

 Iterators.dfy(37,14): Error BP5002: A precondition for this call might not hold.

 Iterators.dfy(1,10): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon37_Then

+    (0,0): anon35_Then

     (0,0): anon2

-    (0,0): anon38_Then

+    (0,0): anon36_Then

     (0,0): anon5

-    (0,0): anon39_Then

+    (0,0): anon37_Then

 Iterators.dfy(86,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -1769,11 +1795,11 @@ Execution trace:
 Iterators.dfy(231,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Iterators.dfy(222,3): anon15_LoopHead

-    (0,0): anon15_LoopBody

-    Iterators.dfy(222,3): anon16_Else

-    Iterators.dfy(222,3): anon19_Else

-    (0,0): anon20_Else

+    Iterators.dfy(222,3): anon14_LoopHead

+    (0,0): anon14_LoopBody

+    Iterators.dfy(222,3): anon15_Else

+    Iterators.dfy(222,3): anon18_Else

+    (0,0): anon19_Else

 

 Dafny program verifier finished with 38 verified, 11 errors

 

@@ -1784,18 +1810,22 @@ Dafny program verifier finished with 11 verified, 0 errors
 -------------------- RankNeg.dfy --------------------

 RankNeg.dfy(7,26): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

 RankNeg.dfy(12,28): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

 RankNeg.dfy(19,31): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

 RankNeg.dfy(29,25): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

 

@@ -1808,6 +1838,7 @@ Dafny program verifier finished with 46 verified, 0 errors
 -------------------- ComputationsNeg.dfy --------------------

 ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 ComputationsNeg.dfy(8,1): Error BP5003: A postcondition might not hold on this return path.

 ComputationsNeg.dfy(7,17): Related location: This is the postcondition that might not hold.

@@ -1836,6 +1867,7 @@ Verifying CheckWellformed$$_0_M0.C.Q ...
 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

 

 Verifying CheckWellformed$$_0_M0.C.R ...

@@ -1843,6 +1875,7 @@ Verifying CheckWellformed$$_0_M0.C.R ...
 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon5_Else

 

 Verifying CheckWellformed$$_1_M1.C.M ...

@@ -1856,6 +1889,7 @@ Verifying CheckWellformed$$_1_M1.C.P ...
 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy[M1](19,26): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

@@ -1874,14 +1908,17 @@ Execution trace:
     (0,0): anon0

 SmallTests.dfy(61,36): Error: possible division by zero

 Execution trace:

+    (0,0): anon0

     (0,0): anon12_Then

 SmallTests.dfy(62,51): Error: possible division by zero

 Execution trace:

+    (0,0): anon0

     (0,0): anon12_Else

     (0,0): anon3

     (0,0): anon13_Else

 SmallTests.dfy(63,22): Error: target object may be null

 Execution trace:

+    (0,0): anon0

     (0,0): anon12_Then

     (0,0): anon3

     (0,0): anon13_Then

@@ -1889,9 +1926,9 @@ Execution trace:
 SmallTests.dfy(82,24): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(81,5): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    (0,0): anon10_Then

+    SmallTests.dfy(81,5): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    (0,0): anon9_Then

 SmallTests.dfy(116,5): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -1945,6 +1982,7 @@ Execution trace:
     (0,0): anon0

 SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 SmallTests.dfy(669,14): Error: assertion violation

 Execution trace:

@@ -1979,10 +2017,12 @@ Execution trace:
     (0,0): anon0

 SmallTests.dfy(343,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 SmallTests.dfy(387,10): Error BP5003: A postcondition might not hold on this return path.

 SmallTests.dfy(390,41): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon6_Else

 SmallTests.dfy(540,12): Error: assertion violation

 Execution trace:

@@ -2054,14 +2094,17 @@ Execution trace:
     (0,0): anon0

 out.tmp.dfy(69,37): Error: possible division by zero

 Execution trace:

+    (0,0): anon0

     (0,0): anon12_Then

 out.tmp.dfy(70,52): Error: possible division by zero

 Execution trace:

+    (0,0): anon0

     (0,0): anon12_Else

     (0,0): anon3

     (0,0): anon13_Else

 out.tmp.dfy(71,22): Error: target object may be null

 Execution trace:

+    (0,0): anon0

     (0,0): anon12_Then

     (0,0): anon3

     (0,0): anon13_Then

@@ -2069,9 +2112,9 @@ Execution trace:
 out.tmp.dfy(88,24): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    out.tmp.dfy(87,5): anon9_LoopHead

-    (0,0): anon9_LoopBody

-    (0,0): anon10_Then

+    out.tmp.dfy(87,5): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    (0,0): anon9_Then

 out.tmp.dfy(122,5): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -2125,6 +2168,7 @@ Execution trace:
     (0,0): anon0

 out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 out.tmp.dfy(388,14): Error: assertion violation

 Execution trace:

@@ -2159,10 +2203,12 @@ Execution trace:
     (0,0): anon0

 out.tmp.dfy(490,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

+    (0,0): anon0

     (0,0): anon3_Else

 out.tmp.dfy(498,10): Error BP5003: A postcondition might not hold on this return path.

 out.tmp.dfy(499,41): Related location: This is the postcondition that might not hold.

 Execution trace:

+    (0,0): anon0

     (0,0): anon6_Else

 out.tmp.dfy(536,12): Error: assertion violation

 Execution trace: