Dafny: keep counters for loops, temporary variables across two implementations in the refinement VC

1 files changed, 13 insertions, 2 deletions

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index e417ac68..5a762ef6 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1807,11 +1807,16 @@ namespace Microsoft.Dafny {
         assert var != null;

         builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, var)));

       }

+

+      // set-up method-translator state

+      currentMethod = m;

+      loopHeapVarCount = 0;

+      otherTmpVarCount = 0;

+      _phvie = null;

+      _nwie = null;

             

       //  call inlined m;      

-      currentMethod = m;

       TrStmt(m.Body, builder, localVariables, etran);

-      currentMethod = null;

 

       //  $Heap1 := $Heap;

       Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));

@@ -1825,7 +1830,13 @@ namespace Microsoft.Dafny {
       currentMethod = r;

       etran = new ExpressionTranslator(this, predef, heap, "this");

       TrStmt(r.Body, builder, localVariables, etran);

+

+      // clean method-translator state

       currentMethod = null;

+      loopHeapVarCount = 0;

+      otherTmpVarCount = 0;

+      _phvie = null;

+      _nwie = null;

       

       //  assert output variables of r and m are pairwise equal

       assert outParams.Length % 2 == 0;