Penetrating by blocks

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -829,7 +829,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
                         // use the given assert attribute only
                         builder.Add(Assert(tok, ss.E, desc, builder.Context, wfOptions.AssertKv));
                       } else {
-                        builder.Add(AssertAndForget(tok, ss.E, desc));
+                        builder.Add(AssertAndForget(builder.Context, tok, ss.E, desc));
                       }
                     }
                   }
@@ -1665,7 +1665,7 @@ private void CheckElementInit(IToken tok, bool forArray, List<Expression> dims,
       var pre = FunctionCall(tok, Requires(dims.Count), Bpl.Type.Bool, args);
       var q = new Bpl.ForallExpr(tok, bvs, BplImp(ante, pre));
       var indicesDesc = new PODesc.IndicesInDomain(forArray ? "array" : "sequence", dims, init);
-      builder.Add(AssertAndForget(tok, q, indicesDesc));
+      builder.Add(AssertAndForget(builder.Context, tok, q, indicesDesc));
       if (!forArray && options.DoReadsChecks) {
         // unwrap renamed local lambdas
         var unwrappedFunc = init;
@@ -1716,7 +1716,7 @@ private void CheckElementInit(IToken tok, bool forArray, List<Expression> dims,
         // assert (forall i0,i1,i2,... ::
         //            0 <= i0 < ... && ... ==> init.requires(i0,i1,i2,...) is Subtype);
         q = new Bpl.ForallExpr(tok, bvs, BplImp(ante, cre));
-        builder.Add(AssertAndForget(init.tok, q, subrangeDesc));
+        builder.Add(AssertAndForget(builder.Context, init.tok, q, subrangeDesc));
       }
 
       if (forArray) {

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -1576,7 +1576,7 @@ private void SplitAndAssertExpression(BoogieStmtListBuilder witnessCheckBuilder,
       foreach (var split in ss) {
         if (split.IsChecked) {
           var tok = witnessExpr.tok is { } t ? new NestedToken(t, split.Tok) : witnessExpr.tok;
-          witnessCheckBuilder.Add(AssertAndForget(tok, split.E, desc));
+          witnessCheckBuilder.Add(AssertAndForget(witnessCheckBuilder.Context, tok, split.E, desc));
         }
       }
     }

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -3362,18 +3362,19 @@ private PredicateCmd Assert(IToken tok, Expr condition, PODesc.ProofObligationDe
       return cmd;
     }
 
-    Bpl.PredicateCmd AssertAndForget(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc) {
-      return AssertAndForget(tok, condition, desc, tok, null);
+    PredicateCmd AssertAndForget(BodyTranslationContext context, IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc) {
+      return AssertAndForget(context, tok, condition, desc, tok, null);
     }
 
-    Bpl.PredicateCmd AssertAndForget(IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc, IToken refinesTok, Bpl.QKeyValue kv) {
+    PredicateCmd AssertAndForget(BodyTranslationContext context, IToken tok, Bpl.Expr condition, PODesc.ProofObligationDescription desc, IToken refinesTok, Bpl.QKeyValue kv) {
       Contract.Requires(tok != null);
       Contract.Requires(desc != null);
       Contract.Requires(condition != null);
       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
 
-      Bpl.PredicateCmd cmd;
-      if ((assertionOnlyFilter != null && !assertionOnlyFilter(tok)) ||
+      PredicateCmd cmd;
+      if (context.AssertMode == AssertMode.Assume ||
+          (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) ||
           (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
         // produce a "skip" instead
         cmd = TrAssumeCmd(tok, Bpl.Expr.True, kv);
@@ -3502,7 +3503,8 @@ Bpl.AssertCmd TrAssertCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes =
       return attributes == null ? new Bpl.AssertCmd(tok, expr) : new Bpl.AssertCmd(tok, expr, attributes);
     }
 
-    Bpl.AssertCmd TrAssertCmdDesc(IToken tok, Bpl.Expr expr, PODesc.ProofObligationDescription description, Bpl.QKeyValue attributes = null) {
+    Bpl.AssertCmd TrAssertCmdDesc(IToken tok, Bpl.Expr expr, 
+      PODesc.ProofObligationDescription description, Bpl.QKeyValue attributes = null) {
       ReportAssertion(tok, description);
       return new Bpl.AssertCmd(tok, expr, description, attributes);
     }

Source/DafnyCore/Verifier/Statements/BlockByProofStmtVerifier.cs

@@ -9,9 +9,9 @@ public static void EmitBoogie(BoogieGenerator generator, BlockByProofStmt block,
     List<Variable> locals, BoogieGenerator.ExpressionTranslator etran, ICodeContext codeContext) {
     var proofBuilder = new BoogieStmtListBuilder(generator, builder.Options, builder.Context);
 
-    //generator.CurrentIdGenerator.Push();
+    generator.CurrentIdGenerator.Push();
     generator.TrStmtList(block.Proof.Body, proofBuilder, locals, etran);
-    //generator.CurrentIdGenerator.Pop();
+    generator.CurrentIdGenerator.Pop();
 
     generator.TrStmt(block.Body, proofBuilder, locals, etran);
     generator.PathAsideBlock(block.Tok, proofBuilder, builder);

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs

@@ -346,7 +346,8 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
     }
 
     AddReferencedMember(callee);
-    var call = Call(builder.Context, tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCall : MethodTranslationKind.Call), ins, new List<Bpl.IdentifierExpr>());
+    var calleeName = MethodName(callee, isCoCall ? MethodTranslationKind.CoCall : MethodTranslationKind.Call);
+    var call = Call(builder.Context, tok, calleeName, ins, outs);
     proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs));
     if (
       (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) ||

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs

@@ -173,7 +173,7 @@ private bool TrAssertCondition(PredicateStmt stmt,
           if (split.IsChecked) {
             var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
             var desc = new PODesc.AssertStatementDescription(stmt, errorMessage, successMessage);
-            proofBuilder.Add(AssertAndForget(ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
+            proofBuilder.Add(AssertAndForget(proofBuilder.Context, ToDafnyToken(flags.ReportRanges, tok), split.E, desc, stmt.Tok,
               etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
           }
         }

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs

@@ -131,7 +131,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder,
           } else if (split.IsChecked) {
             var yieldToken = new NestedToken(s.Tok, split.Tok);
             var desc = new PODesc.YieldEnsures(fieldSub.Substitute(p.E));
-            builder.Add(AssertAndForget(yieldToken, split.E, desc, stmt.Tok, null));
+            builder.Add(AssertAndForget(builder.Context, yieldToken, split.E, desc, stmt.Tok, null));
           }
         }
         builder.Add(TrAssumeCmdWithDependencies(yeEtran, stmt.Tok, p.E, "yield ensures clause"));
@@ -585,19 +585,19 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, List<Varia
             TrStmt_CheckWellformed(index, b, locals, etran, false);
             if (index.Type.IsNumericBased(Type.NumericPersuasion.Int)) {
               var desc = new PODesc.PrefixEqualityLimit(index);
-              b.Add(AssertAndForget(index.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(index)), desc));
+              b.Add(AssertAndForget(b.Context, index.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(index)), desc));
             }
           }
           TrStmt_CheckWellformed(CalcStmt.Rhs(stmt.Steps[i]), b, locals, etran, false);
           var ss = TrSplitExpr(builder.Context, stmt.Steps[i], etran, true, out var splitHappened);
           // assert step:
           AddComment(b, stmt, "assert line" + i.ToString() + " " + (stmt.StepOps[i] ?? stmt.Op).ToString() + " line" + (i + 1).ToString());
           if (!splitHappened) {
-            b.Add(AssertAndForget(stmt.Lines[i + 1].tok, etran.TrExpr(stmt.Steps[i]), new PODesc.CalculationStep(stmt.Steps[i], stmt.Hints[i])));
+            b.Add(AssertAndForget(b.Context, stmt.Lines[i + 1].tok, etran.TrExpr(stmt.Steps[i]), new PODesc.CalculationStep(stmt.Steps[i], stmt.Hints[i])));
           } else {
             foreach (var split in ss) {
               if (split.IsChecked) {
-                b.Add(AssertAndForget(stmt.Lines[i + 1].tok, split.E, new PODesc.CalculationStep(stmt.Steps[i], stmt.Hints[i])));
+                b.Add(AssertAndForget(b.Context, stmt.Lines[i + 1].tok, split.E, new PODesc.CalculationStep(stmt.Steps[i], stmt.Hints[i])));
               }
             }
           }

Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s"
+// RUN: %testDafnyForEachResolver "%s" -- --bprint=/Users/rwillems/SourceCode/dafny/b4.bpl
 
 
 // Note: We are using the built-in equality to compare keys.