12 files changed, 1924 insertions, 131 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 52f52abf..c7552a79 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));
       }
@@ -4555,7 +4555,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)));
           }
@@ -4691,7 +4691,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) {
@@ -4720,7 +4720,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;
@@ -4734,7 +4734,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)));
             }
@@ -4755,7 +4755,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;
@@ -4781,7 +4781,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;
       }
@@ -4793,7 +4793,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>
@@ -4852,7 +4852,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)));
@@ -5048,7 +5048,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
@@ -5087,7 +5087,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) {
@@ -5148,7 +5148,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;
@@ -5245,7 +5245,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;
@@ -5276,7 +5276,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) {
@@ -5284,9 +5284,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"));
           }
@@ -5295,11 +5295,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;
           }
         }
@@ -5406,7 +5406,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
@@ -5460,11 +5460,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)));
       }
     }
 
@@ -6499,7 +6499,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);
         }
@@ -6984,9 +6984,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;
       }
@@ -7003,12 +7003,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;
       }
@@ -7022,9 +7022,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;
       }
@@ -7097,13 +7097,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) {
@@ -7161,7 +7161,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
@@ -7180,7 +7180,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);
@@ -7245,7 +7245,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) {
@@ -7320,7 +7320,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);
@@ -7383,11 +7383,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);
@@ -7486,7 +7486,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());
@@ -7514,7 +7514,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();
           }
@@ -7523,12 +7523,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();
@@ -7539,7 +7539,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) {
@@ -7617,7 +7617,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
@@ -7632,7 +7632,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
@@ -7656,7 +7656,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) {
@@ -7738,7 +7738,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));
@@ -7953,7 +7953,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);
@@ -7989,7 +7989,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) {
@@ -7998,7 +7998,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;
@@ -8011,7 +8011,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
 
@@ -8019,7 +8019,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 ::
@@ -8046,7 +8046,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) {
@@ -8055,7 +8055,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));
         }
       } 
     }
@@ -8158,18 +8158,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.
@@ -8186,7 +8186,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) {
@@ -8214,7 +8214,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>();
@@ -8242,7 +8242,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));
         }       
       }
     }
@@ -8309,10 +8309,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);
@@ -8330,7 +8330,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.
 
@@ -8344,7 +8344,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));
         }
       }
 
@@ -8352,9 +8352,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));
       }
     }
 
@@ -8379,6 +8379,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);
 
@@ -8427,11 +8436,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);
@@ -8444,7 +8453,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));
               }
             }
           }
@@ -8460,14 +8469,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
@@ -8481,13 +8490,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;
@@ -8528,13 +8537,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);
 
@@ -8569,7 +8578,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 {
@@ -8838,7 +8847,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);
         }
       }
@@ -8866,7 +8875,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;
@@ -9792,7 +9801,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
@@ -9817,13 +9826,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++;
           }
         }
@@ -9929,7 +9938,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>
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 9e36e64c..9891c040 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C {
diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
index d32cd9bb..bf7388cf 100644
--- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> DoNothingToAssert
-Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
+Processing command (at Snapshots0.v0.dfy(4,10)) assert false;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 3 verified, 0 errors
@@ -16,7 +16,7 @@ Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f
   >>> MarkAsFullyVerified
 Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);
   >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
+Processing command (at Snapshots0.v1.dfy(4,10)) assert false;
   >>> MarkAsPartiallyVerified
 Snapshots0.v1.dfy(4,9): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
index 6d5e43f8..1b5c8d24 100644
--- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> DoNothingToAssert
-Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
+Processing command (at Snapshots1.v0.dfy(4,10)) assert false;
   >>> DoNothingToAssert
 Processing command (at Snapshots1.v0.dfy(12,3)) assert true;
   >>> DoNothingToAssert
@@ -12,7 +12,7 @@ Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
   >>> MarkAsFullyVerified
 Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> MarkAsFullyVerified
-Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
+Processing command (at Snapshots1.v1.dfy(4,10)) assert false;
   >>> DoNothingToAssert
 Snapshots1.v1.dfy(4,9): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
index ee2ceecd..949ecec9 100644
--- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
@@ -1,6 +1,6 @@
 Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
+Processing command (at Snapshots2.v0.dfy(4,10)) assert false;
   >>> DoNothingToAssert
 Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
   >>> DoNothingToAssert
@@ -24,7 +24,7 @@ Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
   >>> MarkAsFullyVerified
 Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
   >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
+Processing command (at Snapshots2.v1.dfy(4,10)) assert false;
   >>> DoNothingToAssert
 Snapshots2.v1.dfy(4,9): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
index accacd90..a7f05a68 100644
--- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
@@ -1,4 +1,4 @@
-Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);
+Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0;
   >>> DoNothingToAssert
 Snapshots3.v0.dfy(9,13): Error: assertion violation
 Execution trace:
@@ -6,9 +6,9 @@ Execution trace:
     (0,0): anon3_Else
 
 Dafny program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);
+Processing command (at Snapshots3.v1.dfy(5,12)) assert true;
   >>> DoNothingToAssert
-Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);
+Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0;
   >>> RecycleError
 Snapshots3.v0.dfy(9,13): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
index d56eb9d0..e0f07849 100644
--- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
@@ -2,11 +2,11 @@ Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 2 verified, 0 errors
-Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);
+Processing command (at Snapshots4.v1.dfy(5,14)) assert 1 != 1;
   >>> DoNothingToAssert
 Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);
   >>> MarkAsFullyVerified
-Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);
+Processing command (at Snapshots4.v1.dfy(10,14)) assert 2 != 2;
   >>> DoNothingToAssert
 Snapshots4.v1.dfy(5,13): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
index bef5a87d..cdb942bb 100644
--- a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
@@ -1,8 +1,8 @@
-Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false);
+Processing command (at Snapshots6.v0.dfy(20,14)) assert false;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 4 verified, 0 errors
-Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);
+Processing command (at Snapshots6.v1.dfy(20,14)) assert false;
   >>> DoNothingToAssert
 Snapshots6.v1.dfy(20,13): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
index b90a6034..a08b32c6 100644
--- a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
@@ -1,4 +1,4 @@
-Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false);
+Processing command (at Snapshots7.v0.dfy(19,14)) assert false;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 4 verified, 0 errors
@@ -22,7 +22,7 @@ Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##ext
   >>> AssumeNegationOfAssumptionVariable
 Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##4();
   >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);
+Processing command (at Snapshots7.v1.dfy(19,14)) assert false;
   >>> MarkAsPartiallyVerified
 Snapshots7.v1.dfy(19,13): Error: assertion violation
 Execution trace:
diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
index 625b71b4..e1cbdbe0 100644
--- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect
@@ -20,7 +20,7 @@ Snapshots8.v0.dfy(13,12): Related location: This is the postcondition that might
 Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(23,11): Error: assertion violation
-Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true);
+Processing command (at Snapshots8.v0.dfy(28,10)) assert true;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 7 verified, 4 errors
@@ -45,7 +45,7 @@ Snapshots8.v1.dfy(12,20): Related location: This is the precondition that might
 Snapshots8.v1.dfy(7,11): Error: assertion violation
 Processing command (at Snapshots8.v1.dfy(21,12)) assert true;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true);
+Processing command (at Snapshots8.v1.dfy(23,12)) assert true;
   >>> DoNothingToAssert
 Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0;
   >>> DoNothingToAssert
diff --git a/Test/dafny4/Bug136.dfy b/Test/dafny4/Bug136.dfy
new file mode 100644
index 00000000..5f3cde69
--- /dev/null
+++ b/Test/dafny4/Bug136.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:0 /print:- "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method test()
+{
+    assume false;
+    assert true;
+}
+
+
+
+
diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect
new file mode 100644
index 00000000..8b9d32a8
--- /dev/null
+++ b/Test/dafny4/Bug136.dfy.expect
@@ -0,0 +1,1772 @@
+// Dafny program verifier version 1.9.6.21116, Copyright (c) 2003-2015, Microsoft.
+// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /compile:0 /print:- c:\dafny\Test\dafny4\Bug136.dfy
+
+const $$Language$Dafny: bool;
+
+axiom $$Language$Dafny;
+
+type Ty;
+
+const unique TBool: Ty;
+
+const unique TChar: Ty;
+
+const unique TInt: Ty;
+
+const unique TNat: Ty;
+
+const unique TReal: Ty;
+
+function TSet(Ty) : Ty;
+
+function TISet(Ty) : Ty;
+
+function TMultiSet(Ty) : Ty;
+
+function TSeq(Ty) : Ty;
+
+function TMap(Ty, Ty) : Ty;
+
+function TIMap(Ty, Ty) : Ty;
+
+function Inv0_TSet(Ty) : Ty;
+
+axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);
+
+function Inv0_TISet(Ty) : Ty;
+
+axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);
+
+function Inv0_TSeq(Ty) : Ty;
+
+axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);
+
+function Inv0_TMultiSet(Ty) : Ty;
+
+axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t);
+
+function Inv0_TMap(Ty) : Ty;
+
+function Inv1_TMap(Ty) : Ty;
+
+axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv0_TMap(TMap(t, u)) == t);
+
+axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv1_TMap(TMap(t, u)) == u);
+
+function Inv0_TIMap(Ty) : Ty;
+
+function Inv1_TIMap(Ty) : Ty;
+
+axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv0_TIMap(TIMap(t, u)) == t);
+
+axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv1_TIMap(TIMap(t, u)) == u);
+
+type TyTag;
+
+function Tag(Ty) : TyTag;
+
+const unique TagBool: TyTag;
+
+const unique TagChar: TyTag;
+
+const unique TagInt: TyTag;
+
+const unique TagNat: TyTag;
+
+const unique TagReal: TyTag;
+
+const unique TagSet: TyTag;
+
+const unique TagISet: TyTag;
+
+const unique TagMultiSet: TyTag;
+
+const unique TagSeq: TyTag;
+
+const unique TagMap: TyTag;
+
+const unique TagIMap: TyTag;
+
+const unique TagClass: TyTag;
+
+axiom Tag(TBool) == TagBool;
+
+axiom Tag(TChar) == TagChar;
+
+axiom Tag(TInt) == TagInt;
+
+axiom Tag(TNat) == TagNat;
+
+axiom Tag(TReal) == TagReal;
+
+axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet);
+
+axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet);
+
+axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);
+
+axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq);
+
+axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Tag(TMap(t, u)) == TagMap);
+
+axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Tag(TIMap(t, u)) == TagIMap);
+
+function {:identity} LitInt(x: int) : int;
+
+axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x);
+
+axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)));
+
+function {:identity} LitReal(x: real) : real;
+
+axiom (forall x: real :: {:identity} { LitReal(x): real } LitReal(x): real == x);
+
+axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)));
+
+function {:identity} Lit<T>(x: T) : T;
+
+axiom (forall<T> x: T :: {:identity} { Lit(x): T } Lit(x): T == x);
+
+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)));
+
+type char;
+
+function char#FromInt(int) : char;
+
+function char#ToInt(char) : int;
+
+axiom (forall ch: char :: { char#ToInt(ch) } char#FromInt(char#ToInt(ch)) == ch);
+
+axiom (forall n: int :: 
+  { char#FromInt(n) } 
+  0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);
+
+type ref;
+
+const null: ref;
+
+const unique NoTraitAtAll: ClassName;
+
+function TraitParent(ClassName) : ClassName;
+
+type Box;
+
+const $ArbitraryBoxValue: Box;
+
+function $Box<T>(T) : Box;
+
+function $Unbox<T>(Box) : T;
+
+axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
+
+axiom (forall bx: Box :: 
+  { $IsBox(bx, TInt) } 
+  $IsBox(bx, TInt) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TInt));
+
+axiom (forall bx: Box :: 
+  { $IsBox(bx, TNat) } 
+  $IsBox(bx, TNat) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TNat));
+
+axiom (forall bx: Box :: 
+  { $IsBox(bx, TReal) } 
+  $IsBox(bx, TReal)
+     ==> $Box($Unbox(bx): real) == bx && $Is($Unbox(bx): real, TReal));
+
+axiom (forall bx: Box :: 
+  { $IsBox(bx, TBool) } 
+  $IsBox(bx, TBool)
+     ==> $Box($Unbox(bx): bool) == bx && $Is($Unbox(bx): bool, TBool));
+
+axiom (forall bx: Box :: 
+  { $IsBox(bx, TChar) } 
+  $IsBox(bx, TChar)
+     ==> $Box($Unbox(bx): char) == bx && $Is($Unbox(bx): char, TChar));
+
+axiom (forall bx: Box, t: Ty :: 
+  { $IsBox(bx, TSet(t)) } 
+  $IsBox(bx, TSet(t))
+     ==> $Box($Unbox(bx): Set Box) == bx && $Is($Unbox(bx): Set Box, TSet(t)));
+
+axiom (forall bx: Box, t: Ty :: 
+  { $IsBox(bx, TISet(t)) } 
+  $IsBox(bx, TISet(t))
+     ==> $Box($Unbox(bx): ISet Box) == bx && $Is($Unbox(bx): ISet Box, TISet(t)));
+
+axiom (forall bx: Box, t: Ty :: 
+  { $IsBox(bx, TMultiSet(t)) } 
+  $IsBox(bx, TMultiSet(t))
+     ==> $Box($Unbox(bx): MultiSet Box) == bx
+       && $Is($Unbox(bx): MultiSet Box, TMultiSet(t)));
+
+axiom (forall bx: Box, t: Ty :: 
+  { $IsBox(bx, TSeq(t)) } 
+  $IsBox(bx, TSeq(t))
+     ==> $Box($Unbox(bx): Seq Box) == bx && $Is($Unbox(bx): Seq Box, TSeq(t)));
+
+axiom (forall bx: Box, s: Ty, t: Ty :: 
+  { $IsBox(bx, TMap(s, t)) } 
+  $IsBox(bx, TMap(s, t))
+     ==> $Box($Unbox(bx): Map Box Box) == bx && $Is($Unbox(bx): Map Box Box, TMap(s, t)));
+
+axiom (forall bx: Box, s: Ty, t: Ty :: 
+  { $IsBox(bx, TIMap(s, t)) } 
+  $IsBox(bx, TIMap(s, t))
+     ==> $Box($Unbox(bx): IMap Box Box) == bx
+       && $Is($Unbox(bx): IMap Box Box, TIMap(s, t)));
+
+axiom (forall<T> v: T, t: Ty :: 
+  { $IsBox($Box(v), t) } 
+  $IsBox($Box(v), t) <==> $Is(v, t));
+
+axiom (forall<T> v: T, t: Ty, h: Heap :: 
+  { $IsAllocBox($Box(v), t, h) } 
+  $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v, t, h));
+
+function $Is<T>(T, Ty) : bool;
+
+function $IsAlloc<T>(T, Ty, Heap) : bool;
+
+function $IsBox<T>(T, Ty) : bool;
+
+function $IsAllocBox<T>(T, Ty, Heap) : bool;
+
+axiom (forall v: int :: { $Is(v, TInt) } $Is(v, TInt));
+
+axiom (forall v: int :: { $Is(v, TNat) } $Is(v, TNat) <==> v >= 0);
+
+axiom (forall v: real :: { $Is(v, TReal) } $Is(v, TReal));
+
+axiom (forall v: bool :: { $Is(v, TBool) } $Is(v, TBool));
+
+axiom (forall v: char :: { $Is(v, TChar) } $Is(v, TChar));
+
+axiom (forall h: Heap, v: int :: { $IsAlloc(v, TInt, h) } $IsAlloc(v, TInt, h));
+
+axiom (forall h: Heap, v: int :: { $IsAlloc(v, TNat, h) } $IsAlloc(v, TNat, h));
+
+axiom (forall h: Heap, v: real :: { $IsAlloc(v, TReal, h) } $IsAlloc(v, TReal, h));
+
+axiom (forall h: Heap, v: bool :: { $IsAlloc(v, TBool, h) } $IsAlloc(v, TBool, h));
+
+axiom (forall h: Heap, v: char :: { $IsAlloc(v, TChar, h) } $IsAlloc(v, TChar, h));
+
+axiom (forall v: Set Box, t0: Ty :: 
+  { $Is(v, TSet(t0)) } 
+  $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));
+
+axiom (forall v: ISet Box, t0: Ty :: 
+  { $Is(v, TISet(t0)) } 
+  $Is(v, TISet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));
+
+axiom (forall v: MultiSet Box, t0: Ty :: 
+  { $Is(v, TMultiSet(t0)) } 
+  $Is(v, TMultiSet(t0))
+     <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsBox(bx, t0)));
+
+axiom (forall v: MultiSet Box, t0: Ty :: 
+  { $Is(v, TMultiSet(t0)) } 
+  $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v));
+
+axiom (forall v: Seq Box, t0: Ty :: 
+  { $Is(v, TSeq(t0)) } 
+  $Is(v, TSeq(t0))
+     <==> (forall i: int :: 
+      { Seq#Index(v, i) } 
+      0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0)));
+
+axiom (forall v: Set Box, t0: Ty, h: Heap :: 
+  { $IsAlloc(v, TSet(t0), h) } 
+  $IsAlloc(v, TSet(t0), h)
+     <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: ISet Box, t0: Ty, h: Heap :: 
+  { $IsAlloc(v, TISet(t0), h) } 
+  $IsAlloc(v, TISet(t0), h)
+     <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: 
+  { $IsAlloc(v, TMultiSet(t0), h) } 
+  $IsAlloc(v, TMultiSet(t0), h)
+     <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: Seq Box, t0: Ty, h: Heap :: 
+  { $IsAlloc(v, TSeq(t0), h) } 
+  $IsAlloc(v, TSeq(t0), h)
+     <==> (forall i: int :: 
+      { Seq#Index(v, i) } 
+      0 <= i && i < Seq#Length(v) ==> $IsAllocBox(Seq#Index(v, i), t0, h)));
+
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty :: 
+  { $Is(v, TMap(t0, t1)) } 
+  $Is(v, TMap(t0, t1))
+     <==> (forall bx: Box :: 
+      { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } 
+      Map#Domain(v)[bx] ==> $IsBox(Map#Elements(v)[bx], t1) && $IsBox(bx, t0)));
+
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap :: 
+  { $IsAlloc(v, TMap(t0, t1), h) } 
+  $IsAlloc(v, TMap(t0, t1), h)
+     <==> (forall bx: Box :: 
+      { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } 
+      Map#Domain(v)[bx]
+         ==> $IsAllocBox(Map#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty :: 
+  { $Is(v, TIMap(t0, t1)) } 
+  $Is(v, TIMap(t0, t1))
+     <==> (forall bx: Box :: 
+      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } 
+      IMap#Domain(v)[bx] ==> $IsBox(IMap#Elements(v)[bx], t1) && $IsBox(bx, t0)));
+
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap :: 
+  { $IsAlloc(v, TIMap(t0, t1), h) } 
+  $IsAlloc(v, TIMap(t0, t1), h)
+     <==> (forall bx: Box :: 
+      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } 
+      IMap#Domain(v)[bx]
+         ==> $IsAllocBox(IMap#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));
+
+type ClassName;
+
+const unique class._System.int: ClassName;
+
+const unique class._System.bool: ClassName;
+
+const unique class._System.set: ClassName;
+
+const unique class._System.seq: ClassName;
+
+const unique class._System.multiset: ClassName;
+
+function Tclass._System.object() : Ty;
+
+function dtype(ref) : Ty;
+
+function TypeTuple(a: ClassName, b: ClassName) : ClassName;
+
+function TypeTupleCar(ClassName) : ClassName;
+
+function TypeTupleCdr(ClassName) : ClassName;
+
+axiom (forall a: ClassName, b: ClassName :: 
+  { TypeTuple(a, b) } 
+  TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b);
+
+type HandleType;
+
+function SetRef_to_SetBox(s: [ref]bool) : Set Box;
+
+axiom (forall s: [ref]bool, bx: Box :: 
+  { SetRef_to_SetBox(s)[bx] } 
+  SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);
+
+axiom (forall s: [ref]bool :: 
+  { SetRef_to_SetBox(s) } 
+  $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));
+
+type DatatypeType;
+
+type DtCtorId;
+
+function DatatypeCtorId(DatatypeType) : DtCtorId;
+
+function DtRank(DatatypeType) : int;
+
+function BoxRank(Box) : int;
+
+axiom (forall d: DatatypeType :: { BoxRank($Box(d)) } BoxRank($Box(d)) == DtRank(d));
+
+const $ModuleContextHeight: int;
+
+const $FunctionContextHeight: int;
+
+type LayerType;
+
+const $LZ: LayerType;
+
+function $LS(LayerType) : LayerType;
+
+function AtLayer<A>([LayerType]A, LayerType) : A;
+
+axiom (forall<A> f: [LayerType]A, ly: LayerType :: 
+  { AtLayer(f, ly) } 
+  AtLayer(f, ly) == f[ly]);
+
+axiom (forall<A> f: [LayerType]A, ly: LayerType :: 
+  { AtLayer(f, $LS(ly)) } 
+  AtLayer(f, $LS(ly)) == AtLayer(f, ly));
+
+type Field _;
+
+function FDim<T>(Field T) : int;
+
+function IndexField(int) : Field Box;
+
+axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);
+
+function IndexField_Inverse<T>(Field T) : int;
+
+axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
+
+function MultiIndexField(Field Box, int) : Field Box;
+
+axiom (forall f: Field Box, i: int :: 
+  { MultiIndexField(f, i) } 
+  FDim(MultiIndexField(f, i)) == FDim(f) + 1);
+
+function MultiIndexField_Inverse0<T>(Field T) : Field T;
+
+function MultiIndexField_Inverse1<T>(Field T) : int;
+
+axiom (forall f: Field Box, i: int :: 
+  { MultiIndexField(f, i) } 
+  MultiIndexField_Inverse0(MultiIndexField(f, i)) == f
+     && MultiIndexField_Inverse1(MultiIndexField(f, i)) == i);
+
+function DeclType<T>(Field T) : ClassName;
+
+type NameFamily;
+
+function DeclName<T>(Field T) : NameFamily;
+
+function FieldOfDecl<alpha>(ClassName, NameFamily) : Field alpha;
+
+axiom (forall<T> cl: ClassName, nm: NameFamily :: 
+  { FieldOfDecl(cl, nm): Field T } 
+  DeclType(FieldOfDecl(cl, nm): Field T) == cl
+     && DeclName(FieldOfDecl(cl, nm): Field T) == nm);
+
+function $IsGhostField<T>(Field T) : bool;
+
+axiom (forall<T> h: Heap, k: Heap, v: T, t: Ty :: 
+  { $HeapSucc(h, k), $IsAlloc(v, t, h) } 
+  $HeapSucc(h, k) ==> $IsAlloc(v, t, h) ==> $IsAlloc(v, t, k));
+
+axiom (forall h: Heap, k: Heap, bx: Box, t: Ty :: 
+  { $HeapSucc(h, k), $IsAllocBox(bx, t, h) } 
+  $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k));
+
+const unique alloc: Field bool;
+
+axiom FDim(alloc) == 0 && !$IsGhostField(alloc);
+
+function _System.array.Length(a: ref) : int;
+
+axiom (forall o: ref :: 0 <= _System.array.Length(o));
+
+function Int(x: real) : int;
+
+axiom (forall x: real :: { Int(x): int } Int(x): int == int(x));
+
+function Real(x: int) : real;
+
+axiom (forall x: int :: { Real(x): real } Real(x): real == real(x));
+
+axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i);
+
+function {:inline true} _System.real.Trunc(x: real) : int
+{
+  Int(x)
+}
+
+type Heap = <alpha>[ref,Field alpha]alpha;
+
+function {:inline true} read<alpha>(H: Heap, r: ref, f: Field alpha) : alpha
+{
+  H[r, f]
+}
+
+function {:inline true} update<alpha>(H: Heap, r: ref, f: Field alpha, v: alpha) : Heap
+{
+  H[r, f := v]
+}
+
+function $IsGoodHeap(Heap) : bool;
+
+function $IsHeapAnchor(Heap) : bool;
+
+var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
+
+function $HeapSucc(Heap, Heap) : bool;
+
+axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha :: 
+  { update(h, r, f, x) } 
+  $IsGoodHeap(update(h, r, f, x)) ==> $HeapSucc(h, update(h, r, f, x)));
+
+axiom (forall a: Heap, b: Heap, c: Heap :: 
+  { $HeapSucc(a, b), $HeapSucc(b, c) } 
+  $HeapSucc(a, b) && $HeapSucc(b, c) ==> $HeapSucc(a, c));
+
+axiom (forall h: Heap, k: Heap :: 
+  { $HeapSucc(h, k) } 
+  $HeapSucc(h, k)
+     ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
+
+function $HeapSuccGhost(Heap, Heap) : bool;
+
+axiom (forall h: Heap, k: Heap :: 
+  { $HeapSuccGhost(h, k) } 
+  $HeapSuccGhost(h, k)
+     ==> $HeapSucc(h, k)
+       && (forall<alpha> o: ref, f: Field alpha :: 
+        { read(k, o, f) } 
+        !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
+
+type TickType;
+
+var $Tick: TickType;
+
+procedure $YieldHavoc(this: ref, rds: Set Box, nw: Set Box);
+  modifies $Heap;
+  ensures (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> 
+    $o == this || rds[$Box($o)] || nw[$Box($o)]
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure $IterHavoc0(this: ref, rds: Set Box, modi: Set Box);
+  modifies $Heap;
+  ensures (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> 
+    rds[$Box($o)] && !modi[$Box($o)] && $o != this
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box);
+  modifies $Heap;
+  ensures (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)
+       || $o == this
+       || modi[$Box($o)]
+       || nw[$Box($o)]);
+  ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box))
+   returns (s: Set Box);
+  ensures (forall bx: Box :: 
+  { s[bx] } 
+  s[bx]
+     <==> read(newHeap, this, NW)[bx]
+       || (
+        $Unbox(bx) != null
+         && !read(prevHeap, $Unbox(bx): ref, alloc)
+         && read(newHeap, $Unbox(bx): ref, alloc)));
+
+
+
+type Set T = [T]bool;
+
+function Set#Card<T>(Set T) : int;
+
+axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
+
+function Set#Empty<T>() : Set T;
+
+axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
+
+axiom (forall<T> s: Set T :: 
+  { Set#Card(s) } 
+  (Set#Card(s) == 0 <==> s == Set#Empty())
+     && (Set#Card(s) != 0 ==> (exists x: T :: s[x])));
+
+function Set#Singleton<T>(T) : Set T;
+
+axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
+
+axiom (forall<T> r: T, o: T :: 
+  { Set#Singleton(r)[o] } 
+  Set#Singleton(r)[o] <==> r == o);
+
+axiom (forall<T> r: T :: 
+  { Set#Card(Set#Singleton(r)) } 
+  Set#Card(Set#Singleton(r)) == 1);
+
+function Set#UnionOne<T>(Set T, T) : Set T;
+
+axiom (forall<T> a: Set T, x: T, o: T :: 
+  { Set#UnionOne(a, x)[o] } 
+  Set#UnionOne(a, x)[o] <==> o == x || a[o]);
+
+axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]);
+
+axiom (forall<T> a: Set T, x: T, y: T :: 
+  { Set#UnionOne(a, x), a[y] } 
+  a[y] ==> Set#UnionOne(a, x)[y]);
+
+axiom (forall<T> a: Set T, x: T :: 
+  { Set#Card(Set#UnionOne(a, x)) } 
+  a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
+
+axiom (forall<T> a: Set T, x: T :: 
+  { Set#Card(Set#UnionOne(a, x)) } 
+  !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
+
+function Set#Union<T>(Set T, Set T) : Set T;
+
+axiom (forall<T> a: Set T, b: Set T, o: T :: 
+  { Set#Union(a, b)[o] } 
+  Set#Union(a, b)[o] <==> a[o] || b[o]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T :: 
+  { Set#Union(a, b), a[y] } 
+  a[y] ==> Set#Union(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T :: 
+  { Set#Union(a, b), b[y] } 
+  b[y] ==> Set#Union(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Union(a, b) } 
+  Set#Disjoint(a, b)
+     ==> Set#Difference(Set#Union(a, b), a) == b
+       && Set#Difference(Set#Union(a, b), b) == a);
+
+function Set#Intersection<T>(Set T, Set T) : Set T;
+
+axiom (forall<T> a: Set T, b: Set T, o: T :: 
+  { Set#Intersection(a, b)[o] } 
+  Set#Intersection(a, b)[o] <==> a[o] && b[o]);
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Union(Set#Union(a, b), b) } 
+  Set#Union(Set#Union(a, b), b) == Set#Union(a, b));
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Union(a, Set#Union(a, b)) } 
+  Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Intersection(Set#Intersection(a, b), b) } 
+  Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Intersection(a, Set#Intersection(a, b)) } 
+  Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Card(Set#Union(a, b)) } { Set#Card(Set#Intersection(a, b)) } 
+  Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b))
+     == Set#Card(a) + Set#Card(b));
+
+function Set#Difference<T>(Set T, Set T) : Set T;
+
+axiom (forall<T> a: Set T, b: Set T, o: T :: 
+  { Set#Difference(a, b)[o] } 
+  Set#Difference(a, b)[o] <==> a[o] && !b[o]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T :: 
+  { Set#Difference(a, b), b[y] } 
+  b[y] ==> !Set#Difference(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Card(Set#Difference(a, b)) } 
+  Set#Card(Set#Difference(a, b))
+         + Set#Card(Set#Difference(b, a))
+         + Set#Card(Set#Intersection(a, b))
+       == Set#Card(Set#Union(a, b))
+     && Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b)));
+
+function Set#Subset<T>(Set T, Set T) : bool;
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Subset(a, b) } 
+  Set#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));
+
+function Set#Equal<T>(Set T, Set T) : bool;
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Equal(a, b) } 
+  Set#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));
+
+axiom (forall<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b);
+
+function Set#Disjoint<T>(Set T, Set T) : bool;
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { Set#Disjoint(a, b) } 
+  Set#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));
+
+type ISet T = [T]bool;
+
+function ISet#Empty<T>() : Set T;
+
+axiom (forall<T> o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]);
+
+function ISet#UnionOne<T>(ISet T, T) : ISet T;
+
+axiom (forall<T> a: ISet T, x: T, o: T :: 
+  { ISet#UnionOne(a, x)[o] } 
+  ISet#UnionOne(a, x)[o] <==> o == x || a[o]);
+
+axiom (forall<T> a: ISet T, x: T :: { ISet#UnionOne(a, x) } ISet#UnionOne(a, x)[x]);
+
+axiom (forall<T> a: ISet T, x: T, y: T :: 
+  { ISet#UnionOne(a, x), a[y] } 
+  a[y] ==> ISet#UnionOne(a, x)[y]);
+
+function ISet#Union<T>(ISet T, ISet T) : ISet T;
+
+axiom (forall<T> a: ISet T, b: ISet T, o: T :: 
+  { ISet#Union(a, b)[o] } 
+  ISet#Union(a, b)[o] <==> a[o] || b[o]);
+
+axiom (forall<T> a: ISet T, b: ISet T, y: T :: 
+  { ISet#Union(a, b), a[y] } 
+  a[y] ==> ISet#Union(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T :: 
+  { ISet#Union(a, b), b[y] } 
+  b[y] ==> ISet#Union(a, b)[y]);
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Union(a, b) } 
+  ISet#Disjoint(a, b)
+     ==> ISet#Difference(ISet#Union(a, b), a) == b
+       && ISet#Difference(ISet#Union(a, b), b) == a);
+
+function ISet#Intersection<T>(ISet T, ISet T) : ISet T;
+
+axiom (forall<T> a: ISet T, b: ISet T, o: T :: 
+  { ISet#Intersection(a, b)[o] } 
+  ISet#Intersection(a, b)[o] <==> a[o] && b[o]);
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Union(ISet#Union(a, b), b) } 
+  ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b));
+
+axiom (forall<T> a: Set T, b: Set T :: 
+  { ISet#Union(a, ISet#Union(a, b)) } 
+  ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b));
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Intersection(ISet#Intersection(a, b), b) } 
+  ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b));
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Intersection(a, ISet#Intersection(a, b)) } 
+  ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b));
+
+function ISet#Difference<T>(ISet T, ISet T) : ISet T;
+
+axiom (forall<T> a: ISet T, b: ISet T, o: T :: 
+  { ISet#Difference(a, b)[o] } 
+  ISet#Difference(a, b)[o] <==> a[o] && !b[o]);
+
+axiom (forall<T> a: ISet T, b: ISet T, y: T :: 
+  { ISet#Difference(a, b), b[y] } 
+  b[y] ==> !ISet#Difference(a, b)[y]);
+
+function ISet#Subset<T>(ISet T, ISet T) : bool;
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Subset(a, b) } 
+  ISet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));
+
+function ISet#Equal<T>(ISet T, ISet T) : bool;
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Equal(a, b) } 
+  ISet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Equal(a, b) } 
+  ISet#Equal(a, b) ==> a == b);
+
+function ISet#Disjoint<T>(ISet T, ISet T) : bool;
+
+axiom (forall<T> a: ISet T, b: ISet T :: 
+  { ISet#Disjoint(a, b) } 
+  ISet#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));
+
+function Math#min(a: int, b: int) : int;
+
+axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);
+
+axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);
+
+axiom (forall a: int, b: int :: 
+  { Math#min(a, b) } 
+  Math#min(a, b) == a || Math#min(a, b) == b);
+
+function Math#clip(a: int) : int;
+
+axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);
+
+axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0);
+
+type MultiSet T = [T]int;
+
+function $IsGoodMultiSet<T>(ms: MultiSet T) : bool;
+
+axiom (forall<T> ms: MultiSet T :: 
+  { $IsGoodMultiSet(ms) } 
+  $IsGoodMultiSet(ms)
+     <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms)));
+
+function MultiSet#Card<T>(MultiSet T) : int;
+
+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
+
+axiom (forall<T> s: MultiSet T, x: T, n: int :: 
+  { MultiSet#Card(s[x := n]) } 
+  0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n);
+
+function MultiSet#Empty<T>() : MultiSet T;
+
+axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
+
+axiom (forall<T> s: MultiSet T :: 
+  { MultiSet#Card(s) } 
+  (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty())
+     && (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x])));
+
+function MultiSet#Singleton<T>(T) : MultiSet T;
+
+axiom (forall<T> r: T, o: T :: 
+  { MultiSet#Singleton(r)[o] } 
+  (MultiSet#Singleton(r)[o] == 1 <==> r == o)
+     && (MultiSet#Singleton(r)[o] == 0 <==> r != o));
+
+axiom (forall<T> r: T :: 
+  { MultiSet#Singleton(r) } 
+  MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r));
+
+function MultiSet#UnionOne<T>(MultiSet T, T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, x: T, o: T :: 
+  { MultiSet#UnionOne(a, x)[o] } 
+  0 < MultiSet#UnionOne(a, x)[o] <==> o == x || 0 < a[o]);
+
+axiom (forall<T> a: MultiSet T, x: T :: 
+  { MultiSet#UnionOne(a, x) } 
+  MultiSet#UnionOne(a, x)[x] == a[x] + 1);
+
+axiom (forall<T> a: MultiSet T, x: T, y: T :: 
+  { MultiSet#UnionOne(a, x), a[y] } 
+  0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);
+
+axiom (forall<T> a: MultiSet T, x: T, y: T :: 
+  { MultiSet#UnionOne(a, x), a[y] } 
+  x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);
+
+axiom (forall<T> a: MultiSet T, x: T :: 
+  { MultiSet#Card(MultiSet#UnionOne(a, x)) } 
+  MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
+
+function MultiSet#Union<T>(MultiSet T, MultiSet T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: 
+  { MultiSet#Union(a, b)[o] } 
+  MultiSet#Union(a, b)[o] == a[o] + b[o]);
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Card(MultiSet#Union(a, b)) } 
+  MultiSet#Card(MultiSet#Union(a, b)) == MultiSet#Card(a) + MultiSet#Card(b));
+
+function MultiSet#Intersection<T>(MultiSet T, MultiSet T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: 
+  { MultiSet#Intersection(a, b)[o] } 
+  MultiSet#Intersection(a, b)[o] == Math#min(a[o], b[o]));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } 
+  MultiSet#Intersection(MultiSet#Intersection(a, b), b)
+     == MultiSet#Intersection(a, b));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } 
+  MultiSet#Intersection(a, MultiSet#Intersection(a, b))
+     == MultiSet#Intersection(a, b));
+
+function MultiSet#Difference<T>(MultiSet T, MultiSet T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: 
+  { MultiSet#Difference(a, b)[o] } 
+  MultiSet#Difference(a, b)[o] == Math#clip(a[o] - b[o]));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, y: T :: 
+  { MultiSet#Difference(a, b), b[y], a[y] } 
+  a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0);
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Card(MultiSet#Difference(a, b)) } 
+  MultiSet#Card(MultiSet#Difference(a, b))
+         + MultiSet#Card(MultiSet#Difference(b, a))
+         + 2 * MultiSet#Card(MultiSet#Intersection(a, b))
+       == MultiSet#Card(MultiSet#Union(a, b))
+     && MultiSet#Card(MultiSet#Difference(a, b))
+       == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b)));
+
+function MultiSet#Subset<T>(MultiSet T, MultiSet T) : bool;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Subset(a, b) } 
+  MultiSet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <= b[o]));
+
+function MultiSet#Equal<T>(MultiSet T, MultiSet T) : bool;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Equal(a, b) } 
+  MultiSet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] == b[o]));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Equal(a, b) } 
+  MultiSet#Equal(a, b) ==> a == b);
+
+function MultiSet#Disjoint<T>(MultiSet T, MultiSet T) : bool;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: 
+  { MultiSet#Disjoint(a, b) } 
+  MultiSet#Disjoint(a, b)
+     <==> (forall o: T :: { a[o] } { b[o] } a[o] == 0 || b[o] == 0));
+
+function MultiSet#FromSet<T>(Set T) : MultiSet T;
+
+axiom (forall<T> s: Set T, a: T :: 
+  { MultiSet#FromSet(s)[a] } 
+  (MultiSet#FromSet(s)[a] == 0 <==> !s[a])
+     && (MultiSet#FromSet(s)[a] == 1 <==> s[a]));
+
+axiom (forall<T> s: Set T :: 
+  { MultiSet#Card(MultiSet#FromSet(s)) } 
+  MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));
+
+function MultiSet#FromSeq<T>(Seq T) : MultiSet T;
+
+axiom (forall<T> s: Seq T :: 
+  { MultiSet#FromSeq(s) } 
+  $IsGoodMultiSet(MultiSet#FromSeq(s)));
+
+axiom (forall<T> s: Seq T :: 
+  { MultiSet#Card(MultiSet#FromSeq(s)) } 
+  MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s));
+
+axiom (forall<T> s: Seq T, v: T :: 
+  { MultiSet#FromSeq(Seq#Build(s, v)) } 
+  MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v));
+
+axiom (forall<T>  :: 
+  MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);
+
+axiom (forall<T> a: Seq T, b: Seq T :: 
+  { MultiSet#FromSeq(Seq#Append(a, b)) } 
+  MultiSet#FromSeq(Seq#Append(a, b))
+     == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)));
+
+axiom (forall<T> s: Seq T, i: int, v: T, x: T :: 
+  { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } 
+  0 <= i && i < Seq#Length(s)
+     ==> MultiSet#FromSeq(Seq#Update(s, i, v))[x]
+       == MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s, i))), 
+        MultiSet#Singleton(v))[x]);
+
+axiom (forall<T> s: Seq T, x: T :: 
+  { MultiSet#FromSeq(s)[x] } 
+  (exists i: int :: 
+      { Seq#Index(s, i) } 
+      0 <= i && i < Seq#Length(s) && x == Seq#Index(s, i))
+     <==> 0 < MultiSet#FromSeq(s)[x]);
+
+type Seq _;
+
+function Seq#Length<T>(Seq T) : int;
+
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
+
+function Seq#Empty<T>() : Seq T;
+
+axiom (forall<T>  :: Seq#Length(Seq#Empty(): Seq T) == 0);
+
+axiom (forall<T> s: Seq T :: 
+  { Seq#Length(s) } 
+  Seq#Length(s) == 0 ==> s == Seq#Empty());
+
+axiom (forall<T> t: Ty :: { $Is(Seq#Empty(): Seq T, t) } $Is(Seq#Empty(): Seq T, t));
+
+function Seq#Singleton<T>(T) : Seq T;
+
+axiom (forall<T> t: T :: 
+  { Seq#Length(Seq#Singleton(t)) } 
+  Seq#Length(Seq#Singleton(t)) == 1);
+
+function Seq#Build<T>(s: Seq T, val: T) : Seq T;
+
+axiom (forall<T> s: Seq T, v: T :: 
+  { Seq#Length(Seq#Build(s, v)) } 
+  Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s));
+
+axiom (forall<T> s: Seq T, i: int, v: T :: 
+  { Seq#Index(Seq#Build(s, v), i) } 
+  (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v)
+     && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i)));
+
+axiom (forall s: Seq Box, bx: Box, t: Ty :: 
+  { $Is(Seq#Build(s, bx), TSeq(t)) } 
+  $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t)));
+
+function Seq#Append<T>(Seq T, Seq T) : Seq T;
+
+axiom (forall<T> s0: Seq T, s1: Seq T :: 
+  { Seq#Length(Seq#Append(s0, s1)) } 
+  Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));
+
+axiom (forall s0: Seq Box, s1: Seq Box, t: Ty :: 
+  { $Is(Seq#Append(s0, s1), t) } 
+  $Is(s0, t) && $Is(s1, t) ==> $Is(Seq#Append(s0, s1), t));
+
+function Seq#Index<T>(Seq T, int) : T;
+
+axiom (forall<T> t: T :: 
+  { Seq#Index(Seq#Singleton(t), 0) } 
+  Seq#Index(Seq#Singleton(t), 0) == t);
+
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: 
+  { Seq#Index(Seq#Append(s0, s1), n) } 
+  (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n))
+     && (Seq#Length(s0) <= n
+       ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
+
+function Seq#Update<T>(Seq T, int, T) : Seq T;
+
+axiom (forall<T> s: Seq T, i: int, v: T :: 
+  { Seq#Length(Seq#Update(s, i, v)) } 
+  0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s, i, v)) == Seq#Length(s));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: 
+  { Seq#Index(Seq#Update(s, i, v), n) } 
+  0 <= n && n < Seq#Length(s)
+     ==> (i == n ==> Seq#Index(Seq#Update(s, i, v), n) == v)
+       && (i != n ==> Seq#Index(Seq#Update(s, i, v), n) == Seq#Index(s, n)));
+
+function Seq#Contains<T>(Seq T, T) : bool;
+
+axiom (forall<T> s: Seq T, x: T :: 
+  { Seq#Contains(s, x) } 
+  Seq#Contains(s, x)
+     <==> (exists i: int :: 
+      { Seq#Index(s, i) } 
+      0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+axiom (forall<T> x: T :: 
+  { Seq#Contains(Seq#Empty(), x) } 
+  !Seq#Contains(Seq#Empty(), x));
+
+axiom (forall<T> s0: Seq T, s1: Seq T, x: T :: 
+  { Seq#Contains(Seq#Append(s0, s1), x) } 
+  Seq#Contains(Seq#Append(s0, s1), x)
+     <==> Seq#Contains(s0, x) || Seq#Contains(s1, x));
+
+axiom (forall<T> s: Seq T, v: T, x: T :: 
+  { Seq#Contains(Seq#Build(s, v), x) } 
+  Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x));
+
+axiom (forall<T> s: Seq T, n: int, x: T :: 
+  { Seq#Contains(Seq#Take(s, n), x) } 
+  Seq#Contains(Seq#Take(s, n), x)
+     <==> (exists i: int :: 
+      { Seq#Index(s, i) } 
+      0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+axiom (forall<T> s: Seq T, n: int, x: T :: 
+  { Seq#Contains(Seq#Drop(s, n), x) } 
+  Seq#Contains(Seq#Drop(s, n), x)
+     <==> (exists i: int :: 
+      { Seq#Index(s, i) } 
+      0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+function Seq#Equal<T>(Seq T, Seq T) : bool;
+
+axiom (forall<T> s0: Seq T, s1: Seq T :: 
+  { Seq#Equal(s0, s1) } 
+  Seq#Equal(s0, s1)
+     <==> Seq#Length(s0) == Seq#Length(s1)
+       && (forall j: int :: 
+        { Seq#Index(s0, j) } { Seq#Index(s1, j) } 
+        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0, j) == Seq#Index(s1, j)));
+
+axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b);
+
+function Seq#SameUntil<T>(Seq T, Seq T, int) : bool;
+
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: 
+  { Seq#SameUntil(s0, s1, n) } 
+  Seq#SameUntil(s0, s1, n)
+     <==> (forall j: int :: 
+      { Seq#Index(s0, j) } { Seq#Index(s1, j) } 
+      0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j)));
+
+function Seq#Take<T>(s: Seq T, howMany: int) : Seq T;
+
+axiom (forall<T> s: Seq T, n: int :: 
+  { Seq#Length(Seq#Take(s, n)) } 
+  0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n);
+
+axiom (forall<T> s: Seq T, n: int, j: int :: 
+  {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) } 
+  0 <= j && j < n && j < Seq#Length(s)
+     ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j));
+
+function Seq#Drop<T>(s: Seq T, howMany: int) : Seq T;
+
+axiom (forall<T> s: Seq T, n: int :: 
+  { Seq#Length(Seq#Drop(s, n)) } 
+  0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n);
+
+axiom (forall<T> s: Seq T, n: int, j: int :: 
+  {:weight 25} { Seq#Index(Seq#Drop(s, n), j) } 
+  0 <= n && 0 <= j && j < Seq#Length(s) - n
+     ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n));
+
+axiom (forall<T> s: Seq T, n: int, k: int :: 
+  {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) } 
+  0 <= n && n <= k && k < Seq#Length(s)
+     ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k));
+
+axiom (forall<T> s: Seq T, t: Seq T :: 
+  { Seq#Append(s, t) } 
+  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s
+     && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
+
+function Seq#FromArray(h: Heap, a: ref) : Seq Box;
+
+axiom (forall h: Heap, a: ref :: 
+  { Seq#Length(Seq#FromArray(h, a)) } 
+  Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
+
+axiom (forall h: Heap, a: ref :: 
+  { Seq#FromArray(h, a) } 
+  (forall i: int :: 
+    { read(h, a, IndexField(i)) } { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } 
+    0 <= i && i < Seq#Length(Seq#FromArray(h, a))
+       ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
+
+axiom (forall h0: Heap, h1: Heap, a: ref :: 
+  { Seq#FromArray(h1, a), $HeapSucc(h0, h1) } 
+  $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && $HeapSucc(h0, h1)
+       && (forall i: int :: 
+        0 <= i && i < _System.array.Length(a)
+           ==> read(h0, a, IndexField(i)) == read(h1, a, IndexField(i)))
+     ==> Seq#FromArray(h0, a) == Seq#FromArray(h1, a));
+
+axiom (forall h: Heap, i: int, v: Box, a: ref :: 
+  { Seq#FromArray(update(h, a, IndexField(i), v), a) } 
+  0 <= i && i < _System.array.Length(a)
+     ==> Seq#FromArray(update(h, a, IndexField(i), v), a)
+       == Seq#Update(Seq#FromArray(h, a), i, v));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: 
+  { Seq#Take(Seq#Update(s, i, v), n) } 
+  0 <= i && i < n && n <= Seq#Length(s)
+     ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: 
+  { Seq#Take(Seq#Update(s, i, v), n) } 
+  n <= i && i < Seq#Length(s)
+     ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: 
+  { Seq#Drop(Seq#Update(s, i, v), n) } 
+  0 <= n && n <= i && i < Seq#Length(s)
+     ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i - n, v));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: 
+  { Seq#Drop(Seq#Update(s, i, v), n) } 
+  0 <= i && i < n && n < Seq#Length(s)
+     ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
+
+axiom (forall h: Heap, a: ref, n0: int, n1: int :: 
+  { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } 
+  n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a)
+     ==> Seq#Take(Seq#FromArray(h, a), n1)
+       == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field Box)));
+
+axiom (forall<T> s: Seq T, v: T, n: int :: 
+  { Seq#Drop(Seq#Build(s, v), n) } 
+  0 <= n && n <= Seq#Length(s)
+     ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v));
+
+function Seq#Rank<T>(Seq T) : int;
+
+axiom (forall s: Seq Box, i: int :: 
+  { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) } 
+  0 <= i && i < Seq#Length(s)
+     ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, i: int :: 
+  { Seq#Rank(Seq#Drop(s, i)) } 
+  0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, i: int :: 
+  { Seq#Rank(Seq#Take(s, i)) } 
+  0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, i: int, j: int :: 
+  { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) } 
+  0 <= i && i < j && j <= Seq#Length(s)
+     ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, n: int :: 
+  { Seq#Drop(s, n) } 
+  n == 0 ==> Seq#Drop(s, n) == s);
+
+axiom (forall<T> s: Seq T, n: int :: 
+  { Seq#Take(s, n) } 
+  n == 0 ==> Seq#Take(s, n) == Seq#Empty());
+
+axiom (forall<T> s: Seq T, m: int, n: int :: 
+  { Seq#Drop(Seq#Drop(s, m), n) } 
+  0 <= m && 0 <= n && m + n <= Seq#Length(s)
+     ==> Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m + n));
+
+type Map _ _;
+
+function Map#Domain<U,V>(Map U V) : [U]bool;
+
+function Map#Elements<U,V>(Map U V) : [U]V;
+
+function Map#Card<U,V>(Map U V) : int;
+
+axiom (forall<U,V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
+
+function Map#Empty<U,V>() : Map U V;
+
+axiom (forall<U,V> u: U :: 
+  { Map#Domain(Map#Empty(): Map U V)[u] } 
+  !Map#Domain(Map#Empty(): Map U V)[u]);
+
+axiom (forall<U,V> m: Map U V :: 
+  { Map#Card(m) } 
+  (Map#Card(m) == 0 <==> m == Map#Empty())
+     && (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x])));
+
+function Map#Glue<U,V>([U]bool, [U]V, Ty) : Map U V;
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 
+  { Map#Domain(Map#Glue(a, b, t)) } 
+  Map#Domain(Map#Glue(a, b, t)) == a);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 
+  { Map#Elements(Map#Glue(a, b, t)) } 
+  Map#Elements(Map#Glue(a, b, t)) == b);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 
+  { $Is(Map#Glue(a, b, t), t) } 
+  $Is(Map#Glue(a, b, t), t));
+
+function Map#Build<U,V>(Map U V, U, V) : Map U V;
+
+axiom (forall<U,V> m: Map U V, u: U, u': U, v: V :: 
+  { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] } 
+  (u' == u
+       ==> Map#Domain(Map#Build(m, u, v))[u'] && Map#Elements(Map#Build(m, u, v))[u'] == v)
+     && (u' != u
+       ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u']
+         && Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));
+
+axiom (forall<U,V> m: Map U V, u: U, v: V :: 
+  { Map#Card(Map#Build(m, u, v)) } 
+  Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
+
+axiom (forall<U,V> m: Map U V, u: U, v: V :: 
+  { Map#Card(Map#Build(m, u, v)) } 
+  !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
+
+function Map#Equal<U,V>(Map U V, Map U V) : bool;
+
+axiom (forall<U,V> m: Map U V, m': Map U V :: 
+  { Map#Equal(m, m') } 
+  Map#Equal(m, m')
+     <==> (forall u: U :: Map#Domain(m)[u] == Map#Domain(m')[u])
+       && (forall u: U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));
+
+axiom (forall<U,V> m: Map U V, m': Map U V :: 
+  { Map#Equal(m, m') } 
+  Map#Equal(m, m') ==> m == m');
+
+function Map#Disjoint<U,V>(Map U V, Map U V) : bool;
+
+axiom (forall<U,V> m: Map U V, m': Map U V :: 
+  { Map#Disjoint(m, m') } 
+  Map#Disjoint(m, m')
+     <==> (forall o: U :: 
+      { Map#Domain(m)[o] } { Map#Domain(m')[o] } 
+      !Map#Domain(m)[o] || !Map#Domain(m')[o]));
+
+type IMap _ _;
+
+function IMap#Domain<U,V>(IMap U V) : [U]bool;
+
+function IMap#Elements<U,V>(IMap U V) : [U]V;
+
+function IMap#Empty<U,V>() : IMap U V;
+
+axiom (forall<U,V> u: U :: 
+  { IMap#Domain(IMap#Empty(): IMap U V)[u] } 
+  !IMap#Domain(IMap#Empty(): IMap U V)[u]);
+
+function IMap#Glue<U,V>([U]bool, [U]V, Ty) : IMap U V;
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 
+  { IMap#Domain(IMap#Glue(a, b, t)) } 
+  IMap#Domain(IMap#Glue(a, b, t)) == a);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 
+  { IMap#Elements(IMap#Glue(a, b, t)) } 
+  IMap#Elements(IMap#Glue(a, b, t)) == b);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 
+  { $Is(IMap#Glue(a, b, t), t) } 
+  $Is(IMap#Glue(a, b, t), t));
+
+function IMap#Build<U,V>(IMap U V, U, V) : IMap U V;
+
+axiom (forall<U,V> m: IMap U V, u: U, u': U, v: V :: 
+  { IMap#Domain(IMap#Build(m, u, v))[u'] } 
+    { IMap#Elements(IMap#Build(m, u, v))[u'] } 
+  (u' == u
+       ==> IMap#Domain(IMap#Build(m, u, v))[u']
+         && IMap#Elements(IMap#Build(m, u, v))[u'] == v)
+     && (u' != u
+       ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u']
+         && IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u']));
+
+function IMap#Equal<U,V>(IMap U V, IMap U V) : bool;
+
+axiom (forall<U,V> m: IMap U V, m': IMap U V :: 
+  { IMap#Equal(m, m') } 
+  IMap#Equal(m, m')
+     <==> (forall u: U :: IMap#Domain(m)[u] == IMap#Domain(m')[u])
+       && (forall u: U :: 
+        IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u]));
+
+axiom (forall<U,V> m: IMap U V, m': IMap U V :: 
+  { IMap#Equal(m, m') } 
+  IMap#Equal(m, m') ==> m == m');
+
+function INTERNAL_add_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int :: 
+  { INTERNAL_add_boogie(x, y): int } 
+  INTERNAL_add_boogie(x, y): int == x + y);
+
+function INTERNAL_sub_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int :: 
+  { INTERNAL_sub_boogie(x, y): int } 
+  INTERNAL_sub_boogie(x, y): int == x - y);
+
+function INTERNAL_mul_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int :: 
+  { INTERNAL_mul_boogie(x, y): int } 
+  INTERNAL_mul_boogie(x, y): int == x * y);
+
+function INTERNAL_div_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int :: 
+  { INTERNAL_div_boogie(x, y): int } 
+  INTERNAL_div_boogie(x, y): int == x div y);
+
+function INTERNAL_mod_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int :: 
+  { INTERNAL_mod_boogie(x, y): int } 
+  INTERNAL_mod_boogie(x, y): int == x mod y);
+
+function {:never_pattern true} INTERNAL_lt_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int :: 
+  {:never_pattern true} { INTERNAL_lt_boogie(x, y): bool } 
+  INTERNAL_lt_boogie(x, y): bool == (x < y));
+
+function {:never_pattern true} INTERNAL_le_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int :: 
+  {:never_pattern true} { INTERNAL_le_boogie(x, y): bool } 
+  INTERNAL_le_boogie(x, y): bool == (x <= y));
+
+function {:never_pattern true} INTERNAL_gt_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int :: 
+  {:never_pattern true} { INTERNAL_gt_boogie(x, y): bool } 
+  INTERNAL_gt_boogie(x, y): bool == (x > y));
+
+function {:never_pattern true} INTERNAL_ge_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int :: 
+  {:never_pattern true} { INTERNAL_ge_boogie(x, y): bool } 
+  INTERNAL_ge_boogie(x, y): bool == (x >= y));
+
+const unique class._System.object: ClassName;
+
+// Tclass._System.object Tag
+axiom Tag(Tclass._System.object()) == Tagclass._System.object;
+
+const unique Tagclass._System.object: TyTag;
+
+// Box/unbox axiom for Tclass._System.object
+axiom (forall bx: Box :: 
+  { $IsBox(bx, Tclass._System.object()) } 
+  $IsBox(bx, Tclass._System.object())
+     ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.object()));
+
+// object: Class $Is
+axiom (forall $o: ref :: 
+  { $Is($o, Tclass._System.object()) } 
+  $Is($o, Tclass._System.object()));
+
+// object: Class $IsAlloc
+axiom (forall $o: ref, $h: Heap :: 
+  { $IsAlloc($o, Tclass._System.object(), $h) } 
+  $IsAlloc($o, Tclass._System.object(), $h) <==> $o == null || read($h, $o, alloc));
+
+const unique class._System.array: ClassName;
+
+function Tclass._System.array(Ty) : Ty;
+
+// Tclass._System.array Tag
+axiom (forall #$arg: Ty :: 
+  { Tclass._System.array(#$arg) } 
+  Tag(Tclass._System.array(#$arg)) == Tagclass._System.array);
+
+const unique Tagclass._System.array: TyTag;
+
+// Tclass._System.array injectivity 0
+axiom (forall #$arg: Ty :: 
+  { Tclass._System.array(#$arg) } 
+  Tclass._System.array_0(Tclass._System.array(#$arg)) == #$arg);
+
+function Tclass._System.array_0(Ty) : Ty;
+
+// Box/unbox axiom for Tclass._System.array
+axiom (forall #$arg: Ty, bx: Box :: 
+  { $IsBox(bx, Tclass._System.array(#$arg)) } 
+  $IsBox(bx, Tclass._System.array(#$arg))
+     ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.array(#$arg)));
+
+// array.: Allocation axiom
+axiom (forall #$arg: Ty, $i0: int, $h: Heap, $o: ref :: 
+  { read($h, $o, IndexField($i0)), Tclass._System.array(#$arg) } 
+  $IsGoodHeap($h)
+       && $o != null
+       && dtype($o) == Tclass._System.array(#$arg)
+       && 
+      0 <= $i0
+       && $i0 < _System.array.Length($o)
+     ==> $IsBox(read($h, $o, IndexField($i0)), #$arg)
+       && (read($h, $o, alloc) ==> $IsAllocBox(read($h, $o, IndexField($i0)), #$arg, $h)));
+
+// array: Class $Is
+axiom (forall #$arg: Ty, $o: ref :: 
+  { $Is($o, Tclass._System.array(#$arg)) } 
+  $Is($o, Tclass._System.array(#$arg))
+     <==> $o == null || dtype($o) == Tclass._System.array(#$arg));
+
+// array: Class $IsAlloc
+axiom (forall #$arg: Ty, $o: ref, $h: Heap :: 
+  { $IsAlloc($o, Tclass._System.array(#$arg), $h) } 
+  $IsAlloc($o, Tclass._System.array(#$arg), $h)
+     <==> $o == null || read($h, $o, alloc));
+
+// array.Length: Allocation axiom
+axiom (forall #$arg: Ty, $h: Heap, $o: ref :: 
+  $IsGoodHeap($h) && $o != null && dtype($o) == Tclass._System.array(#$arg)
+     ==> $Is(_System.array.Length($o), TInt)
+       && (read($h, $o, alloc) ==> $IsAlloc(_System.array.Length($o), TInt, $h)));
+
+function Tclass._System.___hFunc0(Ty) : Ty;
+
+// Tclass._System.___hFunc0 Tag
+axiom (forall #$T0: Ty :: 
+  { Tclass._System.___hFunc0(#$T0) } 
+  Tag(Tclass._System.___hFunc0(#$T0)) == Tagclass._System.___hFunc0);
+
+const unique Tagclass._System.___hFunc0: TyTag;
+
+// Tclass._System.___hFunc0 injectivity 0
+axiom (forall #$T0: Ty :: 
+  { Tclass._System.___hFunc0(#$T0) } 
+  Tclass._System.___hFunc0_0(Tclass._System.___hFunc0(#$T0)) == #$T0);
+
+function Tclass._System.___hFunc0_0(Ty) : Ty;
+
+// Box/unbox axiom for Tclass._System.___hFunc0
+axiom (forall #$T0: Ty, bx: Box :: 
+  { $IsBox(bx, Tclass._System.___hFunc0(#$T0)) } 
+  $IsBox(bx, Tclass._System.___hFunc0(#$T0))
+     ==> $Box($Unbox(bx): HandleType) == bx
+       && $Is($Unbox(bx): HandleType, Tclass._System.___hFunc0(#$T0)));
+
+function Handle0([Heap]Box, [Heap]bool, [Heap]Set Box) : HandleType;
+
+function Apply0(Ty, HandleType, Heap) : Box;
+
+function Requires0(Ty, HandleType, Heap) : bool;
+
+function Reads0(Ty, HandleType, Heap) : Set Box;
+
+axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box :: 
+  { Apply0(t0, Handle0(h, r, rd), heap) } 
+  Apply0(t0, Handle0(h, r, rd), heap) == h[heap]);
+
+axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box :: 
+  { Requires0(t0, Handle0(h, r, rd), heap) } 
+  r[heap] ==> Requires0(t0, Handle0(h, r, rd), heap));
+
+axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box, bx: Box :: 
+  { Reads0(t0, Handle0(h, r, rd), heap)[bx] } 
+  Reads0(t0, Handle0(h, r, rd), heap)[bx] == rd[heap][bx]);
+
+function {:inline true} _System.___hFunc0.requires(t0: Ty, heap: Heap, f: HandleType) : bool
+{
+  Requires0(t0, f, heap)
+}
+
+function {:inline true} _System.___hFunc0.requires#canCall(t0: Ty, heap: Heap, f: HandleType) : bool
+{
+  true
+}
+
+function {:inline true} _System.___hFunc0.reads(t0: Ty, heap: Heap, f: HandleType) : Set Box
+{
+  Reads0(t0, f, heap)
+}
+
+function {:inline true} _System.___hFunc0.reads#canCall(t0: Ty, heap: Heap, f: HandleType) : bool
+{
+  true
+}
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 
+  { $HeapSucc(h0, h1), Reads0(t0, f, h1) } 
+  $HeapSucc(h0, h1)
+       && 
+      $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+       && (forall<a> o: ref, fld: Field a :: 
+        o != null
+             && read(h0, o, alloc)
+             && read(h1, o, alloc)
+             && Reads0(t0, f, h0)[$Box(o)]
+           ==> read(h0, o, fld) == read(h1, o, fld))
+     ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 
+  { $HeapSucc(h0, h1), Reads0(t0, f, h1) } 
+  $HeapSucc(h0, h1)
+       && 
+      $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+       && (forall<a> o: ref, fld: Field a :: 
+        o != null
+             && read(h0, o, alloc)
+             && read(h1, o, alloc)
+             && Reads0(t0, f, h1)[$Box(o)]
+           ==> read(h0, o, fld) == read(h1, o, fld))
+     ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 
+  { $HeapSucc(h0, h1), Requires0(t0, f, h1) } 
+  $HeapSucc(h0, h1)
+       && 
+      $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+       && (forall<a> o: ref, fld: Field a :: 
+        o != null
+             && read(h0, o, alloc)
+             && read(h1, o, alloc)
+             && Reads0(t0, f, h0)[$Box(o)]
+           ==> read(h0, o, fld) == read(h1, o, fld))
+     ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 
+  { $HeapSucc(h0, h1), Requires0(t0, f, h1) } 
+  $HeapSucc(h0, h1)
+       && 
+      $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+       && (forall<a> o: ref, fld: Field a :: 
+        o != null
+             && read(h0, o, alloc)
+             && read(h1, o, alloc)
+             && Reads0(t0, f, h1)[$Box(o)]
+           ==> read(h0, o, fld) == read(h1, o, fld))
+     ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 
+  { $HeapSucc(h0, h1), Apply0(t0, f, h1) } 
+  $HeapSucc(h0, h1)
+       && 
+      $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+       && (forall<a> o: ref, fld: Field a :: 
+        o != null
+             && read(h0, o, alloc)
+             && read(h1, o, alloc)
+             && Reads0(t0, f, h0)[$Box(o)]
+           ==> read(h0, o, fld) == read(h1, o, fld))
+     ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 
+  { $HeapSucc(h0, h1), Apply0(t0, f, h1) } 
+  $HeapSucc(h0, h1)
+       && 
+      $IsGoodHeap(h0)
+       && $IsGoodHeap(h1)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+       && (forall<a> o: ref, fld: Field a :: 
+        o != null
+             && read(h0, o, alloc)
+             && read(h1, o, alloc)
+             && Reads0(t0, f, h1)[$Box(o)]
+           ==> read(h0, o, fld) == read(h1, o, fld))
+     ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));
+
+axiom (forall t0: Ty, h: Heap, f: HandleType :: 
+  { Apply0(t0, f, h) } 
+  $IsGoodHeap(h)
+       && 
+      $Is(f, Tclass._System.___hFunc0(t0))
+       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h)
+     ==> $IsBox(Apply0(t0, f, h), t0) && $IsAllocBox(Apply0(t0, f, h), t0, h));
+
+const unique class._module.__default: ClassName;
+
+function Tclass._module.__default() : Ty;
+
+// Tclass._module.__default Tag
+axiom Tag(Tclass._module.__default()) == Tagclass._module.__default;
+
+const unique Tagclass._module.__default: TyTag;
+
+// Box/unbox axiom for Tclass._module.__default
+axiom (forall bx: Box :: 
+  { $IsBox(bx, Tclass._module.__default()) } 
+  $IsBox(bx, Tclass._module.__default())
+     ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._module.__default()));
+
+// _default: Class $Is
+axiom (forall $o: ref :: 
+  { $Is($o, Tclass._module.__default()) } 
+  $Is($o, Tclass._module.__default())
+     <==> $o == null || dtype($o) == Tclass._module.__default());
+
+// _default: Class $IsAlloc
+axiom (forall $o: ref, $h: Heap :: 
+  { $IsAlloc($o, Tclass._module.__default(), $h) } 
+  $IsAlloc($o, Tclass._module.__default(), $h)
+     <==> $o == null || read($h, $o, alloc));
+
+procedure CheckWellformed$$_module.__default.test();
+  free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
+  modifies $Heap, $Tick;
+
+
+
+implementation CheckWellformed$$_module.__default.test()
+{
+  var $_Frame: <beta>[ref,Field beta]bool;
+
+    // AddMethodImpl: test, CheckWellformed$$_module.__default.test
+    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
+  $o != null && read($Heap, $o, alloc) ==> false);
+    assume {:captureState "Bug136.dfy(4,7): initial state"} true;
+    havoc $Heap;
+    assume (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+    assume $HeapSucc(old($Heap), $Heap);
+}
+
+
+
+procedure InterModuleCall$$_module.__default.test();
+  modifies $Heap, $Tick;
+  // frame condition
+  free ensures (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  // boilerplate
+  free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure IntraModuleCall$$_module.__default.test();
+  modifies $Heap, $Tick;
+  // frame condition
+  free ensures (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  // boilerplate
+  free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure Impl$$_module.__default.test() returns ($_reverifyPost: bool);
+  free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
+  modifies $Heap, $Tick;
+  // frame condition
+  free ensures (forall<alpha> $o: ref, $f: Field alpha :: 
+  { read($Heap, $o, $f) } 
+  $o != null && read(old($Heap), $o, alloc)
+     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+  // boilerplate
+  free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+implementation Impl$$_module.__default.test() returns ($_reverifyPost: bool)
+{
+  var $_Frame: <beta>[ref,Field beta]bool;
+
+    // AddMethodImpl: test, Impl$$_module.__default.test
+    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
+  $o != null && read($Heap, $o, alloc) ==> false);
+    assume {:captureState "Bug136.dfy(5,1): initial state"} true;
+    $_reverifyPost := false;
+    // ----- assume statement ----- Bug136.dfy(6,5)
+    assume true;
+    assume false;
+    // ----- assert statement ----- Bug136.dfy(7,5)
+    assume true;
+    assert true;
+}
+
+
+
+Dafny program verifier finished with 2 verified, 0 errors