Merge

4 files changed, 143 insertions, 128 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index f5f95bd2..d6b2d9ba 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -937,10 +937,10 @@ namespace Microsoft.Dafny {
         Error("Method {0} has no body", wr, m.FullName);

       } else {

         if (m.IsTailRecursive) {

-          Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");

           if (!m.IsStatic) {

             Indent(indent + IndentAmount, wr); wr.WriteLine("var _this = this;");

           }

+          Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");

         }

         Contract.Assert(enclosingMethod == null);

         enclosingMethod = m;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 80792ce2..af7082a4 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2064,9 +2064,10 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
   "case"                      (. x = t; .)

   ( Ident<out id>             (. name = id.val; .)

     [ "("

-      CasePattern<out pat>        (. arguments.Add(pat); .)

-      { "," CasePattern<out pat>  (. arguments.Add(pat); .)

-      }

+       [ CasePattern<out pat>        (. arguments.Add(pat); .)

+         { "," CasePattern<out pat>  (. arguments.Add(pat); .)

+         }

+       ]

     ")" ]

   | "("

       CasePattern<out pat>        (. arguments.Add(pat); .)

@@ -2881,9 +2882,10 @@ CaseExpression<out MatchCaseExpr c, bool allowSemi, bool allowLambda>
   "case"                      (. x = t; .)

   ( Ident<out id>             (. name = id.val; .)

     [ "("

-      CasePattern<out pat>        (. arguments.Add(pat); .)

-      { "," CasePattern<out pat>  (. arguments.Add(pat); .)

-      }

+       [ CasePattern<out pat>        (. arguments.Add(pat); .)

+         { "," CasePattern<out pat>  (. arguments.Add(pat); .)

+         }

+       ]

     ")" ]

   | "("

       CasePattern<out pat>        (. arguments.Add(pat); .)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 8a1da161..f64ba7fa 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -3244,12 +3244,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			name = id.val; 

 			if (la.kind == 50) {

 				Get();

-				CasePattern(out pat);

-				arguments.Add(pat); 

-				while (la.kind == 22) {

-					Get();

+				if (la.kind == 1 || la.kind == 50) {

 					CasePattern(out pat);

 					arguments.Add(pat); 

+					while (la.kind == 22) {

+						Get();

+						CasePattern(out pat);

+						arguments.Add(pat); 

+					}

 				}

 				Expect(51);

 			}

@@ -4562,12 +4564,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			name = id.val; 

 			if (la.kind == 50) {

 				Get();

-				CasePattern(out pat);

-				arguments.Add(pat); 

-				while (la.kind == 22) {

-					Get();

+				if (la.kind == 1 || la.kind == 50) {

 					CasePattern(out pat);

 					arguments.Add(pat); 

+					while (la.kind == 22) {

+						Get();

+						CasePattern(out pat);

+						arguments.Add(pat); 

+					}

 				}

 				Expect(51);

 			}

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e164d8ee..940bb328 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1650,7 +1650,7 @@ namespace Microsoft.Dafny {
 

       // Next, we assume about this.* whatever we said that the iterator constructor promises

       foreach (var p in iter.Member_Init.Ens) {

-        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+        builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

 

       // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies - {this})

@@ -1676,7 +1676,7 @@ namespace Microsoft.Dafny {
         validCall.TypeArgumentSubstitutions[p] = new UserDefinedType(p);

       } // resolved here.

 

-      builder.Add(new Bpl.AssumeCmd(iter.tok, etran.TrExpr(validCall)));

+      builder.Add(TrAssumeCmd(iter.tok, etran.TrExpr(validCall)));

 

       // check well-formedness of the user-defined part of the yield-requires

       foreach (var p in iter.YieldRequires) {

@@ -1703,13 +1703,13 @@ namespace Microsoft.Dafny {
       setDiff.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference; setDiff.Type = nw.Type;  // resolve here

       Expression cond = new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Fresh, setDiff);

       cond.Type = Type.Bool;  // resolve here

-      builder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(cond)));

+      builder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(cond)));

 

       // check wellformedness of postconditions

       var yeBuilder = new Bpl.StmtListBuilder();

       var endBuilder = new Bpl.StmtListBuilder();

       // In the yield-ensures case:  assume this.Valid();

-      yeBuilder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(validCall)));

+      yeBuilder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(validCall)));

       Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count);

       for (int i = 0; i < iter.OutsFields.Count; i++) {

         var y = iter.OutsFields[i];

@@ -1726,9 +1726,9 @@ namespace Microsoft.Dafny {
         concat.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat; concat.Type = oldThisYs.Type;  // resolve here

 

         // In the yield-ensures case:  assume this.ys == old(this.ys) + [this.y];

-        yeBuilder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat))));

+        yeBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat))));

         // In the ensures case:  assume this.ys == old(this.ys);

-        endBuilder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs))));

+        endBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs))));

       }

 

       foreach (var p in iter.YieldEnsures) {

@@ -1775,18 +1775,18 @@ namespace Microsoft.Dafny {
       // add locals for the yield-history variables and the extra variables

       // Assume the precondition and postconditions of the iterator constructor method

       foreach (var p in iter.Member_Init.Req) {

-        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+        builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

       foreach (var p in iter.Member_Init.Ens) {

         // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet

-        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+        builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E)));

       }

       // add the _yieldCount variable, and assume its initial value to be 0

       yieldCountVariable = new Bpl.LocalVariable(iter.tok,

         new Bpl.TypedIdent(iter.tok, iter.YieldCountVariable.AssignUniqueName(currentDeclaration.IdGenerator), TrType(iter.YieldCountVariable.Type)));

       yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran);  // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption

       localVariables.Add(yieldCountVariable);

-      builder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0))));

+      builder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0))));

       // add a variable $_OldIterHeap

       var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType);

       Bpl.Expr wh = BplAnd(

@@ -2789,7 +2789,7 @@ namespace Microsoft.Dafny {
             if (dt != null) {

               var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool));

               var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));

-              builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List<Bpl.Expr> { f })));

+              builder.Add(TrAssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List<Bpl.Expr> { f })));

             }

           }

 

@@ -2891,7 +2891,7 @@ namespace Microsoft.Dafny {
         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old))

         {

           if (tri.IsFree) {

-            builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));

+            builder.Add(TrAssumeCmd(m.tok, tri.Expr));

           }

         }

 

@@ -3092,7 +3092,7 @@ namespace Microsoft.Dafny {
         //generating class post-conditions

         foreach (var en in f.Ens)

         {

-            builder.Add(new Bpl.AssumeCmd(f.tok, etran.TrExpr(en)));

+            builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en)));

         }

 

         //generating assume J.F(ins) == C.F(ins)

@@ -3117,7 +3117,7 @@ namespace Microsoft.Dafny {
         }

         Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);

         Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);

-        builder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, funcExpT)));

+        builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, funcExpT)));

 

         //generating trait post-conditions with class variables

         foreach (var en in f.OverriddenFunction.Ens)

@@ -3127,7 +3127,7 @@ namespace Microsoft.Dafny {
             var reqSplitedE = TrSplitExpr(postcond, etran,false, out splitHappened);

             foreach (var s in reqSplitedE)

             {

-                var assert = new Bpl.AssertCmd(f.tok, s.E);

+                var assert = TrAssertCmd(f.tok, s.E);

                 assert.ErrorData = "Error: the function must provide an equal or more detailed postcondition than in its parent trait";

                 builder.Add(assert);

             }

@@ -3143,7 +3143,7 @@ namespace Microsoft.Dafny {
         {

             if (tri.IsFree)

             {

-                builder.Add(new Bpl.AssumeCmd(f.tok, tri.Expr));

+                builder.Add(TrAssumeCmd(f.tok, tri.Expr));

             }

         }

     }

@@ -3196,7 +3196,7 @@ namespace Microsoft.Dafny {
         foreach (var req in f.OverriddenFunction.Req)

         {

             Expression precond = Substitute(req, null, substMap);

-            builder.Add(new Bpl.AssumeCmd(f.tok, etran.TrExpr(precond)));

+            builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(precond)));

         }

         //generating class pre-conditions

         foreach (var req in f.Req)

@@ -3205,7 +3205,7 @@ namespace Microsoft.Dafny {
             var reqSplitedE = TrSplitExpr(req, etran,false, out splitHappened);

             foreach (var s in reqSplitedE)

             {

-                var assert = new Bpl.AssertCmd(f.tok, s.E);

+                var assert = TrAssertCmd(f.tok, s.E);

                 assert.ErrorData = "Error: the function must provide an equal or more permissive precondition than in its parent trait";

                 builder.Add(assert);

             }

@@ -3295,7 +3295,7 @@ namespace Microsoft.Dafny {
         {

             if (tri.IsFree)

             {

-                builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));

+                builder.Add(TrAssumeCmd(m.tok, tri.Expr));

             }

         }

     }

@@ -3305,7 +3305,7 @@ namespace Microsoft.Dafny {
         //generating class post-conditions

         foreach (var en in m.Ens)

         {

-            builder.Add(new Bpl.AssumeCmd(m.tok, etran.TrExpr(en.E)));

+            builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(en.E)));

         }

         //generating trait post-conditions with class variables

         foreach (var en in m.OverriddenMethod.Ens)

@@ -3315,7 +3315,7 @@ namespace Microsoft.Dafny {
             var reqSplitedE = TrSplitExpr(postcond, etran,false, out splitHappened);

             foreach (var s in reqSplitedE)

             {

-                var assert = new Bpl.AssertCmd(m.tok, s.E);

+                var assert = TrAssertCmd(m.tok, s.E);

                 assert.ErrorData = "Error: the method must provide an equal or more detailed postcondition than in its parent trait";

                 builder.Add(assert);

             }

@@ -3328,7 +3328,7 @@ namespace Microsoft.Dafny {
         foreach (var req in m.OverriddenMethod.Req)

         {

             Expression precond = Substitute(req.E, null, substMap);

-            builder.Add(new Bpl.AssumeCmd(m.tok, etran.TrExpr(precond)));

+            builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(precond)));

         }

         //generating class pre-conditions

         foreach (var req in m.Req)

@@ -3337,7 +3337,7 @@ namespace Microsoft.Dafny {
             var reqSplitedE = TrSplitExpr(req.E, etran,false, out splitHappened);

             foreach (var s in reqSplitedE)

             {

-                var assert = new Bpl.AssertCmd(m.tok, s.E);

+                var assert = TrAssertCmd(m.tok, s.E);

                 assert.ErrorData = "Error: the method must provide an equal or more permissive precondition than in its parent trait";

                 builder.Add(assert);

             }

@@ -3617,7 +3617,7 @@ namespace Microsoft.Dafny {
       var col = tok.col + (isEndToken ? tok.val.Length : 0);

       string description = ErrorReporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, col, additionalInfo ?? "");

       QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);

-      return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

+      return TrAssumeCmd(tok, Bpl.Expr.True, kv);

     }

     Bpl.Cmd CaptureState(Statement stmt) {

       Contract.Requires(stmt != null);

@@ -4086,7 +4086,7 @@ namespace Microsoft.Dafny {
 

         var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);

         if (wh != null) {

-          postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, wh));

+          postCheckBuilder.Add(TrAssumeCmd(f.tok, wh));

         }

       }

       // Now for the ensures clauses

@@ -4098,7 +4098,7 @@ namespace Microsoft.Dafny {
       StmtListBuilder bodyCheckBuilder = new StmtListBuilder();

       if (f.Body == null) {

         // don't fall through to postcondition checks

-        bodyCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));

+        bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False));

       } else {

         Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));

         List<Bpl.Expr> args = new List<Bpl.Expr>();

@@ -4126,7 +4126,7 @@ namespace Microsoft.Dafny {
         wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, bodyCheckBuilder);

       }

       // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch

-      postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));

+      postCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False));

       builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok)));

 

       var s0 = builderInitializationArea.Collect(f.tok);

@@ -4241,7 +4241,7 @@ namespace Microsoft.Dafny {
         Type t = mc.Ctor.Formals[i].Type;

         Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, local), p.Type, etran);

         if (wh != null) {

-          localTypeAssumptions.Add(new Bpl.AssumeCmd(p.tok, wh));

+          localTypeAssumptions.Add(TrAssumeCmd(p.tok, wh));

         }

         args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t));

       }

@@ -4548,7 +4548,7 @@ namespace Microsoft.Dafny {
           var correctConstructor = FunctionCall(pat.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, rhs);

           if (ctor.EnclosingDatatype.Ctors.Count == 1) {

             // There is only one constructor, so the value must have been constructed by it; might as well assume that here.

-            builder.Add(new Bpl.AssumeCmd(pat.tok, correctConstructor));

+            builder.Add(TrAssumeCmd(pat.tok, correctConstructor));

           } else {

             builder.Add(Assert(pat.tok, correctConstructor, string.Format("RHS is not certain to look like the pattern '{0}'", ctor.Name)));

           }

@@ -4684,7 +4684,7 @@ namespace Microsoft.Dafny {
         kv = new Bpl.QKeyValue(expr.tok, "subsumption", args, null);

       }

       CheckWellformed(expr, new WFOptions(kv), locals, builder, etran);

-      builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

+      builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

     }

 

     void CheckWellformedAndAssume(Expression expr, WFOptions options, List<Variable> locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {

@@ -4713,7 +4713,7 @@ namespace Microsoft.Dafny {
               CheckWellformedAndAssume(e.E0, options, locals, bAnd, etran);

               CheckWellformedAndAssume(e.E1, options, locals, bAnd, etran);

               var bImp = new Bpl.StmtListBuilder();

-              bImp.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));

+              bImp.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr)));

               builder.Add(new Bpl.IfCmd(expr.tok, null, bAnd.Collect(expr.tok), null, bImp.Collect(expr.tok)));

             }

             return;

@@ -4727,7 +4727,7 @@ namespace Microsoft.Dafny {
               var b0 = new Bpl.StmtListBuilder();

               CheckWellformedAndAssume(e.E0, options, locals, b0, etran);

               var b1 = new Bpl.StmtListBuilder();

-              b1.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0))));

+              b1.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0))));

               CheckWellformedAndAssume(e.E1, options, locals, b1, etran);

               builder.Add(new Bpl.IfCmd(expr.tok, null, b0.Collect(expr.tok), null, b1.Collect(expr.tok)));

             }

@@ -4748,7 +4748,7 @@ namespace Microsoft.Dafny {
         CheckWellformedAndAssume(e.Test, options, locals, bThn, etran);

         CheckWellformedAndAssume(e.Thn, options, locals, bThn, etran);

         var bEls = new Bpl.StmtListBuilder();

-        bEls.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.Test))));

+        bEls.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.Test))));

         CheckWellformedAndAssume(e.Els, options, locals, bEls, etran);

         builder.Add(new Bpl.IfCmd(expr.tok, null, bThn.Collect(expr.tok), null, bEls.Collect(expr.tok)));

         return;

@@ -4774,7 +4774,7 @@ namespace Microsoft.Dafny {
         if (e is ForallExpr) {

           // Although we do the WF check on the original quantifier, we assume the split one.

           // This ensures that cases like forall x :: x != null && f(x.a) do not fail to verify.

-          builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(e.SplitQuantifierExpression ?? e)));

+          builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(e.SplitQuantifierExpression ?? e)));

         }

         return;

       }

@@ -4786,7 +4786,7 @@ namespace Microsoft.Dafny {
       //       the splitting and proceeded to decompose the full quantifier as

       //       normal. This call to TrExpr, on the other hand, will indeed use the

       //       split quantifier.

-      builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));

+      builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr)));

     }

 

     /// <summary>

@@ -4845,7 +4845,7 @@ namespace Microsoft.Dafny {
           var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj));

           if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) {

             // There is only one constructor, so the value must be been constructed by it; might as well assume that here.

-            builder.Add(new Bpl.AssumeCmd(expr.tok, correctConstructor));

+            builder.Add(TrAssumeCmd(expr.tok, correctConstructor));

           } else {

             builder.Add(Assert(expr.tok, correctConstructor,

               string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name)));

@@ -5041,7 +5041,7 @@ namespace Microsoft.Dafny {
           if (!etran.UsesOldHeap) {

             // the argument can't be assumed to be allocated for the old heap

             builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function"));

-            builder.Add(new Bpl.AssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));

+            builder.Add(TrAssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));

           }

         }

         // Check that every parameter is available in the state in which the function is invoked; this means checking that it has

@@ -5080,7 +5080,7 @@ namespace Microsoft.Dafny {
           }

           if (options.AssertKv == null) {

             // assume only if no given assert attribute is given

-            builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(precond)));

+            builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(precond)));

           }

         }

         if (options.DoReadsChecks) {

@@ -5141,7 +5141,7 @@ namespace Microsoft.Dafny {
         Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullSanitizedName + "#canCall", Bpl.Type.Bool);

         List<Bpl.Expr> args = etran.FunctionInvocationArguments(e, null);

         Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

-        builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));

+        builder.Add(TrAssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));

 

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

@@ -5238,7 +5238,7 @@ namespace Microsoft.Dafny {
             var rIe = new Bpl.IdentifierExpr(pat.tok, r);

             CheckWellformedWithResult(e.RHSs[i], options, rIe, pat.Expr.Type, locals, builder, etran);

             CheckCasePatternShape(pat, rIe, builder);

-            builder.Add(new Bpl.AssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(Substitute(pat.Expr, null, substMap)), rIe)));

+            builder.Add(TrAssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(Substitute(pat.Expr, null, substMap)), rIe)));

           }

           CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran);

           result = null;

@@ -5269,7 +5269,7 @@ namespace Microsoft.Dafny {
             w = BplOr(body, w);

           }

           builder.Add(Assert(e.tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

-          builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(rhs)));

+          builder.Add(TrAssumeCmd(e.tok, etran.TrExpr(rhs)));

           var letBody = Substitute(e.Body, null, substMap);

           CheckWellformed(letBody, options, locals, builder, etran);

           if (e.Constraint_Bounds != null) {

@@ -5277,9 +5277,9 @@ namespace Microsoft.Dafny {
             var substMap_prime = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran);

             var rhs_prime = Substitute(e.RHSs[0], null, substMap_prime);

             var letBody_prime = Substitute(e.Body, null, substMap_prime);

-            builder.Add(new Bpl.AssumeCmd(e.tok, CanCallAssumption(rhs_prime, etran)));

-            builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(rhs_prime)));

-            builder.Add(new Bpl.AssumeCmd(e.tok, CanCallAssumption(letBody_prime, etran)));

+            builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(rhs_prime, etran)));

+            builder.Add(TrAssumeCmd(e.tok, etran.TrExpr(rhs_prime)));

+            builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(letBody_prime, etran)));

             var eq = Expression.CreateEq(letBody, letBody_prime, e.Body.Type);

             builder.Add(Assert(e.tok, etran.TrExpr(eq), "to be compilable, the value of a let-such-that expression must be uniquely determined"));

           }

@@ -5288,11 +5288,11 @@ namespace Microsoft.Dafny {
             Contract.Assert(resultType != null);

             var bResult = etran.TrExpr(letBody);

             CheckSubrange(letBody.tok, bResult, resultType, builder);

-            builder.Add(new Bpl.AssumeCmd(letBody.tok, Bpl.Expr.Eq(result, bResult)));

-            builder.Add(new Bpl.AssumeCmd(letBody.tok, CanCallAssumption(letBody, etran)));

+            builder.Add(TrAssumeCmd(letBody.tok, Bpl.Expr.Eq(result, bResult)));

+            builder.Add(TrAssumeCmd(letBody.tok, CanCallAssumption(letBody, etran)));

             builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression"));

-            builder.Add(new Bpl.AssumeCmd(letBody.tok, MkIsAlloc(result, resultType, etran.HeapExpr)));

-            builder.Add(new Bpl.AssumeCmd(letBody.tok, MkIs(result, resultType)));

+            builder.Add(TrAssumeCmd(letBody.tok, MkIsAlloc(result, resultType, etran.HeapExpr)));

+            builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType)));

             result = null;

           }

         }

@@ -5399,7 +5399,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr src = etran.TrExpr(me.Source);

         Bpl.IfCmd ifCmd = null;

         StmtListBuilder elsBldr = new StmtListBuilder();

-        elsBldr.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.False));

+        elsBldr.Add(TrAssumeCmd(expr.tok, Bpl.Expr.False));

         StmtList els = elsBldr.Collect(expr.tok);

         foreach (var missingCtor in me.MissingCases) {

           // havoc all bound variables

@@ -5453,11 +5453,11 @@ namespace Microsoft.Dafny {
         Contract.Assert(resultType != null);

         var bResult = etran.TrExpr(expr);

         CheckSubrange(expr.tok, bResult, resultType, builder);

-        builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult)));

-        builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

+        builder.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult)));

+        builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

         builder.Add(new CommentCmd("CheckWellformedWithResult: any expression"));

-        builder.Add(new Bpl.AssumeCmd(expr.tok, MkIsAlloc(result, resultType, etran.HeapExpr)));

-        builder.Add(new Bpl.AssumeCmd(expr.tok, MkIs(result, resultType)));

+        builder.Add(TrAssumeCmd(expr.tok, MkIsAlloc(result, resultType, etran.HeapExpr)));

+        builder.Add(TrAssumeCmd(expr.tok, MkIs(result, resultType)));

       }

     }

 

@@ -6492,7 +6492,7 @@ namespace Microsoft.Dafny {
       foreach (var p in m.Ens) {

         bool splitHappened;  // we actually don't care

         foreach (var s in TrSplitExpr(p.E, etran, true, out splitHappened)) {

-          var assert = new Bpl.AssertCmd(method.tok, s.E, ErrorMessageAttribute(s.E.tok, "This is the postcondition that may not hold."));

+          var assert = TrAssertCmd(method.tok, s.E, ErrorMessageAttribute(s.E.tok, "This is the postcondition that may not hold."));

           assert.ErrorData = "Error: A postcondition of the refined method may not hold.";

           builder.Add(assert);

         }

@@ -6977,9 +6977,9 @@ namespace Microsoft.Dafny {
 

       if (assertAsAssume || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) {

         // produce an assume instead

-        return new Bpl.AssumeCmd(tok, condition, kv);

+        return TrAssumeCmd(tok, condition, kv);

       } else {

-        var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);

+        var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

@@ -6996,12 +6996,12 @@ namespace Microsoft.Dafny {
 

       if (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {

         // produce a "skip" instead

-        return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

+        return TrAssumeCmd(tok, Bpl.Expr.True, kv);

       } else {

         tok = ForceCheckToken.Unwrap(tok);

         var args = new List<object>();

         args.Add(Bpl.Expr.Literal(0));

-        Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, new Bpl.QKeyValue(tok, "subsumption", args, kv));

+        Bpl.AssertCmd cmd = TrAssertCmd(tok, condition, new Bpl.QKeyValue(tok, "subsumption", args, kv));

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

@@ -7015,9 +7015,9 @@ namespace Microsoft.Dafny {
 

       if (assertAsAssume || (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {

         // produce an assume instead

-        return new Bpl.AssumeCmd(tok, condition, kv);

+        return TrAssumeCmd(tok, condition, kv);

       } else {

-        var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);

+        var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv);

         cmd.ErrorData = "Error: " + errorMessage;

         return cmd;

       }

@@ -7090,13 +7090,13 @@ namespace Microsoft.Dafny {
                 builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null)));  // attributes go on every split

               }

             }

-            builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

+            builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

           }

         } else if (stmt is AssumeStmt) {

           AddComment(builder, stmt, "assume statement");

           AssumeStmt s = (AssumeStmt)stmt;

           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

-          builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null)));

+          builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null)));

         }

         this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is PrintStmt) {

@@ -7154,7 +7154,7 @@ namespace Microsoft.Dafny {
         var yc = new Bpl.IdentifierExpr(s.Tok, yieldCountVariable);

         var incYieldCount = Bpl.Cmd.SimpleAssign(s.Tok, yc, Bpl.Expr.Binary(s.Tok, Bpl.BinaryOperator.Opcode.Add, yc, Bpl.Expr.Literal(1)));

         builder.Add(incYieldCount);

-        builder.Add(new Bpl.AssumeCmd(s.Tok, YieldCountAssumption(iter, etran)));

+        builder.Add(TrAssumeCmd(s.Tok, YieldCountAssumption(iter, etran)));

         // assume $IsGoodHeap($Heap);

         builder.Add(AssumeGoodHeap(s.Tok, etran));

         // assert YieldEnsures[subst];  // where 'subst' replaces "old(E)" with "E" being evaluated in $_OldIterHeap

@@ -7173,7 +7173,7 @@ namespace Microsoft.Dafny {
                 builder.Add(AssertNS(yieldToken, split.E, "possible violation of yield-ensures condition", stmt.Tok, null));

               }

             }

-            builder.Add(new Bpl.AssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E)));

+            builder.Add(TrAssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E)));

           }

         }

         YieldHavoc(iter.tok, iter, builder, etran);

@@ -7238,7 +7238,7 @@ namespace Microsoft.Dafny {
           builder.Add(Assert(s.Tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

         }

         // End by doing the assume

-        builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));

+        builder.Add(TrAssumeCmd(s.Tok, etran.TrExpr(s.Expr)));

         builder.Add(CaptureState(s));  // just do one capture state--here, at the very end (that is, don't do one before the assume)

 

       } else if (stmt is UpdateStmt) {

@@ -7313,7 +7313,7 @@ namespace Microsoft.Dafny {
         Bpl.IfCmd elsIf = null;

         b = new Bpl.StmtListBuilder();

         if (s.IsExistentialGuard) {

-          b.Add(new Bpl.AssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard))));

+          b.Add(TrAssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard))));

         }

         if (s.Els == null) {

           els = b.Collect(s.Tok);

@@ -7376,11 +7376,11 @@ namespace Microsoft.Dafny {
           // havoc $Heap;

           builder.Add(new Bpl.HavocCmd(s.Tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));

           // assume $HeapSucc(preModifyHeap, $Heap);   OR $HeapSuccGhost

-          builder.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost)));

+          builder.Add(TrAssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost)));

           // assume nothing outside the frame was changed

           var etranPreLoop = new ExpressionTranslator(this, predef, preModifyHeap);

           var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName);

-          builder.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

+          builder.Add(TrAssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

         } else {

           // do the body, but with preModifyHeapVar as the governing frame

           var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName);

@@ -7479,7 +7479,7 @@ namespace Microsoft.Dafny {
             if (s.Steps[i] is BinaryExpr && (((BinaryExpr)s.Steps[i]).ResolvedOp == BinaryExpr.ResolvedOpcode.Imp)) {

               // assume line<i>:

               AddComment(b, stmt, "assume lhs");

-              b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i]))));

+              b.Add(TrAssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i]))));

             }

             // hint:

             AddComment(b, stmt, "Hint" + i.ToString());

@@ -7507,7 +7507,7 @@ namespace Microsoft.Dafny {
                 }

               }

             }

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

+            b.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

             ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);

             CurrentIdGenerator.Pop();

           }

@@ -7516,12 +7516,12 @@ namespace Microsoft.Dafny {
           AddComment(b, stmt, "assert wf[initial]");

           Contract.Assert(s.Result != null); // established by the resolver

           TrStmt_CheckWellformed(CalcStmt.Lhs(s.Result), b, locals, etran, false);

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

+          b.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

           ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);

           builder.Add(ifCmd);

           // assume result:

           if (s.Steps.Count > 1) {

-            builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));

+            builder.Add(TrAssumeCmd(s.Tok, etran.TrExpr(s.Result)));

           }

         }

         CurrentIdGenerator.Pop();

@@ -7532,7 +7532,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr source = etran.TrExpr(s.Source);

 

         var b = new Bpl.StmtListBuilder();

-        b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));

+        b.Add(TrAssumeCmd(stmt.Tok, Bpl.Expr.False));

         Bpl.StmtList els = b.Collect(stmt.Tok);

         Bpl.IfCmd ifCmd = null;

         foreach (var missingCtor in s.MissingCases) {

@@ -7610,7 +7610,7 @@ namespace Microsoft.Dafny {
           builder.Add(new Bpl.HavocCmd(bv.Tok, new List<Bpl.IdentifierExpr> { bIe }));

           Bpl.Expr wh = GetWhereClause(bv.Tok, bIe, bv.Type, etran);

           if (wh != null) {

-            builder.Add(new Bpl.AssumeCmd(bv.Tok, wh));

+            builder.Add(TrAssumeCmd(bv.Tok, wh));

           }

         }

         Contract.Assert(s.LHSs.Count == s.RHSs.Count);  // checked by resolution

@@ -7625,7 +7625,7 @@ namespace Microsoft.Dafny {
           TrStmt_CheckWellformed(s.RHSs[i], builder, locals, etran, false);

           CheckWellformedWithResult(s.RHSs[i], new WFOptions(null, false, false), rIe, pat.Expr.Type, locals, builder, etran);

           CheckCasePatternShape(pat, rIe, builder);

-          builder.Add(new Bpl.AssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(pat.Expr), rIe)));

+          builder.Add(TrAssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(pat.Expr), rIe)));

         }

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement

@@ -7649,7 +7649,7 @@ namespace Microsoft.Dafny {
         iesForHavoc.Add(new Bpl.IdentifierExpr(local.tok, local));

       }

       builderOutsideIfConstruct.Add(new Bpl.HavocCmd(exists.tok, iesForHavoc));

-      builder.Add(new Bpl.AssumeCmd(exists.tok, etran.TrExpr(exists.Term)));

+      builder.Add(TrAssumeCmd(exists.tok, etran.TrExpr(exists.Term)));

     }

 

     void TrStmtList(List<Statement> stmts, Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {

@@ -7731,7 +7731,7 @@ namespace Microsoft.Dafny {
         new List<Bpl.IdentifierExpr>()));

       // assume YieldRequires;

       foreach (var p in iter.YieldRequires) {

-        builder.Add(new Bpl.AssumeCmd(tok, etran.TrExpr(p.E)));

+        builder.Add(TrAssumeCmd(tok, etran.TrExpr(p.E)));

       }

       // $_OldIterHeap := Heap;

       builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr));

@@ -7946,7 +7946,7 @@ namespace Microsoft.Dafny {
       var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);

       Expression range = Substitute(s.Range, null, substMap);

       TrStmt_CheckWellformed(range, definedness, locals, etran, false);

-      definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range)));

+      definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(range)));

 

       var lhs = Substitute(s0.Lhs.Resolved, null, substMap);

       TrStmt_CheckWellformed(lhs, definedness, locals, etran, false);

@@ -7982,7 +7982,7 @@ namespace Microsoft.Dafny {
         var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);

         var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime);

         range = Substitute(s.Range, null, substMapPrime);

-        definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));

+        definedness.Add(TrAssumeCmd(range.tok, etran.TrExpr(range)));

         // assume !(x == x' && y == y');

         Bpl.Expr eqs = Bpl.Expr.True;

         foreach (var bv in s.BoundVars) {

@@ -7991,7 +7991,7 @@ namespace Microsoft.Dafny {
           // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too?

           eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime)));

         }

-        definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs)));

+        definedness.Add(TrAssumeCmd(s.Tok, Bpl.Expr.Not(eqs)));

         Bpl.Expr objPrime, FPrime;

         GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);

         var Rhs = ((ExprRhs)s0.Rhs).Expr;

@@ -8004,7 +8004,7 @@ namespace Microsoft.Dafny {
           "left-hand sides for different forall-statement bound variables may refer to the same location"));

       }

 

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

+      definedness.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

 

       // Now for the translation of the update itself

 

@@ -8012,7 +8012,7 @@ namespace Microsoft.Dafny {
       var prevEtran = new ExpressionTranslator(this, predef, prevHeap);

       updater.Add(Bpl.Cmd.SimpleAssign(s.Tok, prevHeap, etran.HeapExpr));

       updater.Add(new Bpl.HavocCmd(s.Tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr }));

-      updater.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr)));

+      updater.Add(TrAssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr)));

 

       // Here comes:

       //   assume (forall<alpha> o: ref, f: Field alpha ::

@@ -8039,7 +8039,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr body = Bpl.Expr.Or(Bpl.Expr.Eq(heapOF, oldHeapOF), xObjField);

       var tr = new Trigger(s.Tok, true, new List<Expr>() { heapOF });

       Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar }, null, tr, body);

-      updater.Add(new Bpl.AssumeCmd(s.Tok, qq));

+      updater.Add(TrAssumeCmd(s.Tok, qq));

 

       if (s.ForallExpressions != null) {

         foreach (ForallExpr expr in s.ForallExpressions) {

@@ -8048,7 +8048,7 @@ namespace Microsoft.Dafny {
           var e0 = Substitute(((BinaryExpr)term).E0.Resolved, null, substMap);

           var e1 = Substitute(((BinaryExpr)term).E1, null, substMap);

           qq = TrForall_NewValueAssumption(expr.tok, expr.BoundVars, expr.Range, e0, e1, expr.Attributes, etran, prevEtran);

-          updater.Add(new Bpl.AssumeCmd(s.Tok, qq));

+          updater.Add(TrAssumeCmd(s.Tok, qq));

         }

       } 

     }

@@ -8151,18 +8151,18 @@ namespace Microsoft.Dafny {
             havocIds.Add(new Bpl.IdentifierExpr(tok, bv));

           }

           definedness.Add(new Bpl.HavocCmd(tok, havocIds));

-          definedness.Add(new Bpl.AssumeCmd(tok, ante));

+          definedness.Add(TrAssumeCmd(tok, ante));

         }

         TrStmt_CheckWellformed(range, definedness, locals, etran, false);

-        definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));

+        definedness.Add(TrAssumeCmd(range.tok, etran.TrExpr(range)));

         if (additionalRange != null) {

           var es = additionalRange(new Dictionary<IVariable, Expression>(), etran);

-          definedness.Add(new Bpl.AssumeCmd(es.tok, es));

+          definedness.Add(TrAssumeCmd(es.tok, es));

         }

 

         TrStmt(s0, definedness, locals, etran);

 

-        definedness.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.False));

+        definedness.Add(TrAssumeCmd(tok, Bpl.Expr.False));

       }

 

       // Now for the other branch, where the postcondition of the call is exported.

@@ -8179,7 +8179,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(s0.Method.Mod.Expressions.Count == 0);  // checked by the resolver

         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List<FrameExpression>(), s0.IsGhost, initEtran, etran, initEtran)) {

           if (tri.IsFree) {

-            exporter.Add(new Bpl.AssumeCmd(tok, tri.Expr));

+            exporter.Add(TrAssumeCmd(tok, tri.Expr));

           }

         }

         if (codeContext is IteratorDecl) {

@@ -8207,7 +8207,7 @@ namespace Microsoft.Dafny {
             var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type);

             var p = Substitute(e, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions());  // substitute the call's actuals for the method's formals

             qq = callEtran.TrExpr(p, initEtran);

-            exporter.Add(new Bpl.AssumeCmd(tok, qq));

+            exporter.Add(TrAssumeCmd(tok, qq));

           }

         } else {

           var bvars = new List<Variable>();

@@ -8235,7 +8235,7 @@ namespace Microsoft.Dafny {
           // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))'

           // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0))

           qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post));  // SMART_TRIGGER

-          exporter.Add(new Bpl.AssumeCmd(tok, qq));

+          exporter.Add(TrAssumeCmd(tok, qq));

         }       

       }

     }

@@ -8302,10 +8302,10 @@ namespace Microsoft.Dafny {
           havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv));

         }

         definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds));

-        definedness.Add(new Bpl.AssumeCmd(s.Tok, typeAntecedent));

+        definedness.Add(TrAssumeCmd(s.Tok, typeAntecedent));

       }

       TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);

-      definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));

+      definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));

 

       if (s.Body != null) {

         TrStmt(s.Body, definedness, locals, etran);

@@ -8323,7 +8323,7 @@ namespace Microsoft.Dafny {
         }

       }

 

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

+      definedness.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

 

       // Now for the other branch, where the ensures clauses are exported.

 

@@ -8337,7 +8337,7 @@ namespace Microsoft.Dafny {
       exporter.Add(new Bpl.HavocCmd(s.Tok, new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick() }));

       foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, new List<FrameExpression>(), s.IsGhost, initEtran, etran, initEtran)) {

         if (tri.IsFree) {

-          exporter.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

+          exporter.Add(TrAssumeCmd(s.Tok, tri.Expr));

         }

       }

 

@@ -8345,9 +8345,9 @@ namespace Microsoft.Dafny {
       var p = Substitute(s.ForallExpressions[0], null, substMap);

       Bpl.Expr qq = etran.TrExpr(p, initEtran);

       if (s.BoundVars.Count != 0) {

-        exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));

+        exporter.Add(TrAssumeCmd(s.Tok, qq));

       } else {

-        exporter.Add(new Bpl.AssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body));

+        exporter.Add(TrAssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body));

       }

     }

 

@@ -8372,6 +8372,15 @@ namespace Microsoft.Dafny {
       return description;

     }

 

+    Bpl.AssumeCmd TrAssumeCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) {

+      var lit = RemoveLit(expr);

+      return attributes == null ? new Bpl.AssumeCmd(tok, lit) : new Bpl.AssumeCmd(tok, lit, attributes);

+    }

+

+    Bpl.AssertCmd TrAssertCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) {

+      var lit = RemoveLit(expr);

+      return attributes == null ? new Bpl.AssertCmd(tok, lit) : new Bpl.AssertCmd(tok, lit, attributes);

+    }

 

     delegate void BodyTranslator(Bpl.StmtListBuilder builder, ExpressionTranslator etran);

 

@@ -8420,11 +8429,11 @@ namespace Microsoft.Dafny {
       Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();

       foreach (MaybeFreeExpression loopInv in s.Invariants) {

         TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false);

-        invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

+        invDefinednessBuilder.Add(TrAssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

 

-        invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));

+        invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));

         if (loopInv.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

-          invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

+          invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

         } else {

           bool splitHappened;

           var ss = TrSplitExpr(loopInv.E, etran, false, out splitHappened);

@@ -8437,7 +8446,7 @@ namespace Microsoft.Dafny {
               if (split.IsChecked) {

                 invariants.Add(Assert(split.E.tok, wInv, "loop invariant violation"));  // TODO: it would be fine to have this use {:subsumption 0}

               } else {

-                invariants.Add(new Bpl.AssumeCmd(split.E.tok, wInv));

+                invariants.Add(TrAssumeCmd(split.E.tok, wInv));

               }

             }

           }

@@ -8453,14 +8462,14 @@ namespace Microsoft.Dafny {
         // include boilerplate invariants

         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, modifiesClause, s.IsGhost, etranPreLoop, etran, etran.Old)) {

           if (tri.IsFree) {

-            invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

+            invariants.Add(TrAssumeCmd(s.Tok, tri.Expr));

           } else {

             Contract.Assert(tri.ErrorMessage != null);  // follows from BoilerplateTriple invariant

             invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));

           }

         }

         // add a free invariant which says that the heap hasn't changed outside of the modifies clause.

-        invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

+        invariants.Add(TrAssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

       }

 

       // include a free invariant that says that all completed iterations so far have only decreased the termination metric

@@ -8474,13 +8483,13 @@ namespace Microsoft.Dafny {
           decrs.Add(etran.TrExpr(e));

         }

         Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, initDecr, null, null, true, false);

-        invariants.Add(new Bpl.AssumeCmd(s.Tok, decrCheck));

+        invariants.Add(TrAssumeCmd(s.Tok, decrCheck));

       }

 

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

       loopBodyBuilder.Add(CaptureState(s.Tok, true, "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));

+      invDefinednessBuilder.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

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

       // generate:  CheckWellformed(guard); if (!guard) { break; }

       Bpl.Expr guard = null;

@@ -8521,13 +8530,13 @@ namespace Microsoft.Dafny {
           loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg));

         }

       } else {

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

+        loopBodyBuilder.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

         // todo(maria): havoc stuff

       }

       // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check

       // of invariant-maintenance can use the appropriate canCall predicates.

       foreach (MaybeFreeExpression loopInv in s.Invariants) {

-        loopBodyBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran)));

+        loopBodyBuilder.Add(TrAssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran)));

       }

       Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok);

 

@@ -8562,7 +8571,7 @@ namespace Microsoft.Dafny {
 

       var b = new Bpl.StmtListBuilder();

       var elseTok = elseCase0 != null ? elseCase0.tok : elseCase1.tok;

-      b.Add(new Bpl.AssumeCmd(elseTok, noGuard));

+      b.Add(TrAssumeCmd(elseTok, noGuard));

       if (elseCase0 != null) {

         b.Add(elseCase0);

       } else {

@@ -8831,7 +8840,7 @@ namespace Microsoft.Dafny {
           // the out-parameter.

           Bpl.Cmd cmd = new Bpl.HavocCmd(bLhs.tok, new List<Bpl.IdentifierExpr> { bLhs });

           builder.Add(cmd);

-          cmd = new Bpl.AssumeCmd(bLhs.tok, Bpl.Expr.Eq(bLhs, FunctionCall(bLhs.tok, BuiltinFunction.Unbox, TrType(LhsTypes[i]), tmpVarIdE)));

+          cmd = TrAssumeCmd(bLhs.tok, Bpl.Expr.Eq(bLhs, FunctionCall(bLhs.tok, BuiltinFunction.Unbox, TrType(LhsTypes[i]), tmpVarIdE)));

           builder.Add(cmd);

         }

       }

@@ -8859,7 +8868,7 @@ namespace Microsoft.Dafny {
         builder.Add(new Bpl.HavocCmd(bv.tok, new List<Bpl.IdentifierExpr> { bIe }));

         Bpl.Expr wh = GetWhereClause(bv.tok, bIe, local.Type, etran);

         if (wh != null) {

-          builder.Add(new Bpl.AssumeCmd(bv.tok, wh));

+          builder.Add(TrAssumeCmd(bv.tok, wh));

         }

       }

       return substMap;

@@ -9785,7 +9794,7 @@ namespace Microsoft.Dafny {
       } else if (rhs is HavocRhs) {

         builder.Add(new Bpl.HavocCmd(tok, new List<Bpl.IdentifierExpr> { bLhs }));

         var isNat = CheckSubrange_Expr(tok, bLhs, rhsTypeConstraint);

-        builder.Add(new Bpl.AssumeCmd(tok, isNat));

+        builder.Add(TrAssumeCmd(tok, isNat));

         return CondApplyBox(tok, bLhs, rhsTypeConstraint, lhsType);

       } else {

         // x := new Something

@@ -9810,13 +9819,13 @@ namespace Microsoft.Dafny {
         Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);

         Bpl.Expr rightType;

         rightType = etran.GoodRef_(tok, nw, tRhs.Type, true);

-        builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));

+        builder.Add(TrAssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));

         if (tRhs.ArrayDimensions != null) {

           int i = 0;

           foreach (Expression dim in tRhs.ArrayDimensions) {

             // assume Array#Length($nw, i) == arraySize;

             Bpl.Expr arrayLength = ArrayLength(tok, nw, tRhs.ArrayDimensions.Count, i);

-            builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(dim))));

+            builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(dim))));

             i++;

           }

         }

@@ -9922,7 +9931,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Ensures(Contract.Result<AssumeCmd>() != null);

 

-      return new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));

+      return TrAssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));

     }

 

     /// <summary>