Merge my autoTriggers work into the master branch

This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.

1 files changed, 327 insertions, 166 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4d35549c..e295d25a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -114,6 +114,7 @@ namespace Microsoft.Dafny {
     readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();

     readonly ISet<string> abstractTypes = new HashSet<string>();

     readonly ISet<string> opaqueTypes = new HashSet<string>();

+    FuelContext fuelContext = null;

     Program program;

 

     [ContractInvariantMethod]

@@ -625,6 +626,11 @@ namespace Microsoft.Dafny {
     }

     void AddTypeDecl(NewtypeDecl dd) {

       Contract.Requires(dd != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));      

+

+      FuelContext oldFuelContext = this.fuelContext;

+      this.fuelContext = FuelSetting.NewFuelContext(dd);

+

       AddTypeDecl_Aux(dd.tok, dd.FullName, new List<TypeParameter>());

       AddWellformednessCheck(dd);

       // Add $Is and $IsAlloc axioms for the newtype

@@ -668,6 +674,7 @@ namespace Microsoft.Dafny {
 

         sink.AddTopLevelDeclaration(new Bpl.Axiom(dd.tok, BplForall(vars, BplTrigger(is_o), body), name));

       });

+      this.fuelContext = oldFuelContext;

     }

     void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs) {

       Contract.Requires(tok != null);

@@ -1193,7 +1200,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) {

+    public Bpl.Expr LayerSucc(Bpl.Expr e, int amt = 1) {

       if (amt == 0) {

         return e;

       } else if (amt > 0) {

@@ -1313,6 +1320,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(c != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));

 

       sink.AddTopLevelDeclaration(GetClass(c));

       if (c is ArrayClassDecl) {

@@ -1399,6 +1407,9 @@ namespace Microsoft.Dafny {
 

         } else if (member is Function) {

           var f = (Function)member;

+          FuelContext oldFuelContext = this.fuelContext;

+          this.fuelContext = FuelSetting.NewFuelContext(f);

+

           AddClassMember_Function(f);

           if (!IsOpaqueFunction(f) && !f.IsBuiltin && !(f.tok is IncludeToken)) { // Opaque function's well-formedness is checked on the full version

             AddWellformednessCheck(f);

@@ -1411,9 +1422,11 @@ namespace Microsoft.Dafny {
             AddClassMember_Function(cop.PrefixPredicate);

             // skip the well-formedness check, because it has already been done for the fixpoint-predicate

           }

-

+          this.fuelContext = oldFuelContext;

         } else if (member is Method) {

           Method m = (Method)member;

+          FuelContext oldFuelContext = this.fuelContext;

+          this.fuelContext = FuelSetting.NewFuelContext(m);

 

           // wellformedness check for method specification

           if (m.EnclosingClass is IteratorDecl && m == ((IteratorDecl)m.EnclosingClass).Member_MoveNext) {

@@ -1446,7 +1459,7 @@ namespace Microsoft.Dafny {
             sink.AddTopLevelDeclaration(proc);

             AddMethodImpl(m, proc, false);

           }

-

+          this.fuelContext = oldFuelContext;

         } else {

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

         }

@@ -1479,7 +1492,7 @@ namespace Microsoft.Dafny {
       // declare function

       AddFunction(f);

       // add synonym axiom

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         AddSynonymAxiom(f);

       }

       // add frame axiom

@@ -1506,6 +1519,10 @@ namespace Microsoft.Dafny {
 

     void AddIteratorSpecAndBody(IteratorDecl iter) {

       Contract.Requires(iter != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));

+

+      FuelContext oldFuelContext = this.fuelContext;      

+      this.fuelContext = FuelSetting.NewFuelContext(iter);

 

       // wellformedness check for method specification

       Bpl.Procedure proc = AddIteratorProc(iter, MethodTranslationKind.SpecWellformedness);

@@ -1518,6 +1535,7 @@ namespace Microsoft.Dafny {
         // ...and its implementation

         AddIteratorImpl(iter, proc);

       }

+      this.fuelContext = oldFuelContext;

     }

 

     Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {

@@ -1962,7 +1980,7 @@ namespace Microsoft.Dafny {
       var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);

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

       Bpl.BoundVariable layer;

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

         formals.Add(layer);

         // Note, "layer" is not added to "args" here; rather, that's done below, as needed

@@ -2133,7 +2151,7 @@ namespace Microsoft.Dafny {
       var formals = MkTyParamBinders(GetTypeParams(f), out tyargs);

 

       Bpl.BoundVariable layer;

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

         formals.Add(layer);

         // Note, "layer" is not added to "args" here; rather, that's done below, as needed

@@ -2188,13 +2206,6 @@ namespace Microsoft.Dafny {
       foreach (Expression req in f.Req) {

         pre = BplAnd(pre, etran.TrExpr(Substitute(req, null, substMap)));

       }

-      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)

-      ModuleDefinition mod = f.EnclosingClass.Module;

-      Bpl.Expr useViaContext = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? (Bpl.Expr)Bpl.Expr.True :

-        Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight());

-

-      // ante := (useViaContext && typeAnte && pre)

-      ante = BplAnd(useViaContext, BplAnd(ante, pre));

 

       // Add the precondition function and its axiom (which is equivalent to the ante)

       if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {

@@ -2207,14 +2218,21 @@ namespace Microsoft.Dafny {
         }

         var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,

           formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));

-        sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));

-        // you could use it to check that it always works, but it makes VSI-Benchmarks/b3.dfy time out:

-        // ante = appl;

+        // axiom (forall params :: { f#requires(params) }  ante ==> f#requires(params) == pre);

+        sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl),

+          BplImp(ante, Bpl.Expr.Eq(appl, pre)))));

         if (body == null) {

           return null;

         }

       }

 

+      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)

+      ModuleDefinition mod = f.EnclosingClass.Module;

+      Bpl.Expr useViaContext = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? (Bpl.Expr)Bpl.Expr.True :

+        Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight());

+      // ante := (useViaContext && typeAnte && pre)

+      ante = BplAnd(useViaContext, BplAnd(ante, pre));

+

       // useViaCanCall: f#canCall(args)

       Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);

       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs,args));

@@ -2329,7 +2347,7 @@ namespace Microsoft.Dafny {
 

     void AddSynonymAxiom(Function f) {

       Contract.Requires(f != null);

-      Contract.Requires(f.IsRecursive);

+      Contract.Requires(f.IsFuelAware());

       Contract.Requires(sink != null && predef != null);

       // axiom  // layer synonym axiom

       //   (forall s, $Heap, formals ::

@@ -2412,7 +2430,7 @@ namespace Microsoft.Dafny {
       var coArgs = new List<Bpl.Expr>(tyexprs);

       var prefixArgs = new List<Bpl.Expr>(tyexprs);

       var prefixArgsLimited = new List<Bpl.Expr>(tyexprs);

-      if (pp.IsRecursive) {

+      if (pp.IsFuelAware()) {

         var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", predef.LayerType));

         var s = new Bpl.IdentifierExpr(tok, sV);

         var succS = FunctionCall(tok, BuiltinFunction.LayerSucc, null, s);

@@ -3012,7 +3030,7 @@ namespace Microsoft.Dafny {
         AddFunctionOverrideReqsChk(f, builder, etran, substMap);

 

         //adding assert R <= Rank’;

-        AddFunctionOverrideTerminationChk(f, builder, etran, substMap);

+        AddOverrideTerminationChk(f, f.OverriddenFunction, builder, etran, substMap);

 

         //adding assert W <= Frame’

         AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap);

@@ -3085,13 +3103,13 @@ namespace Microsoft.Dafny {
         Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));

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

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

-        if (f.IsRecursive)

+        if (f.IsFuelAware())

         {

-            argsC.Add(etran.LayerN(1));

+            argsC.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

-        if (f.OverriddenFunction.IsRecursive)

+        if (f.OverriddenFunction.IsFuelAware())

         {

-            argsT.Add(etran.LayerN(1));

+          argsT.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

         argsC.Add(etran.HeapExpr);

         argsT.Add(etran.HeapExpr);

@@ -3175,35 +3193,6 @@ namespace Microsoft.Dafny {
         builder.Add(Assert(tok, q, "expression may read an object not in the parent trait context's reads clause", kv));

     }

 

-    private void AddFunctionOverrideTerminationChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)

-    {

-        var decrToks = new List<IToken>();

-        var decrTypes1 = new List<Type>();

-        var decrTypes2 = new List<Type>();

-        var decrClass = new List<Expr>();

-        var decrTrait = new List<Expr>();

-        if (f.Decreases != null)

-        {

-            foreach (var decC in f.Decreases.Expressions)

-            {

-                decrToks.Add(decC.tok);

-                decrTypes1.Add(decC.Type);

-                decrClass.Add(etran.TrExpr(decC));

-            }

-        }

-        if (f.OverriddenFunction.Decreases != null)

-        {

-            foreach (var decT in f.OverriddenFunction.Decreases.Expressions)

-            {

-                var decCNew = Substitute(decT, null, substMap);

-                decrTypes2.Add(decCNew.Type);

-                decrTrait.Add(etran.TrExpr(decCNew));

-            }

-        }

-        var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);

-        builder.Add(new Bpl.AssertCmd(f.tok, decrChk));

-    }

-

     private void AddFunctionOverrideReqsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)

     {

         //generating trait pre-conditions with class variables

@@ -3271,7 +3260,7 @@ namespace Microsoft.Dafny {
         AddMethodOverrideReqsChk(m, builder, etran, substMap);

 

         //adding assert R <= Rank’;

-        AddMethodOverrideTerminationChk(m, builder, etran, substMap);

+        AddOverrideTerminationChk(m, m.OverriddenMethod, builder, etran, substMap);

 

         //adding assert W <= Frame’

         AddMethodOverrideSubsetChk(m, builder, etran, localVariables, substMap);

@@ -3358,14 +3347,15 @@ namespace Microsoft.Dafny {
         }

     }

 

-    private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {

-      Contract.Requires(m != null);

+    private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {

+      Contract.Requires(original != null);

+      Contract.Requires(overryd != null);

       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       Contract.Requires(substMap != null);

       // Note, it is as if the trait's method is calling the class's method.

-      var contextDecreases = m.OverriddenMethod.Decreases.Expressions;

-      var calleeDecreases = m.Decreases.Expressions;

+      var contextDecreases = overryd.Decreases.Expressions;

+      var calleeDecreases = original.Decreases.Expressions;

       // We want to check:  calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches)

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

         // no check needed

@@ -3386,7 +3376,7 @@ namespace Microsoft.Dafny {
           N = i;

           break;

         }

-        toks.Add(new NestedToken(m.tok, e1.tok));

+        toks.Add(new NestedToken(original.Tok, e1.tok));

         types0.Add(e0.Type.NormalizeExpand());

         types1.Add(e1.Type.NormalizeExpand());

         callee.Add(etran.TrExpr(e0));

@@ -3419,7 +3409,7 @@ namespace Microsoft.Dafny {
       //   as "false".

       bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;

       var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false);

-      builder.Add(Assert(m.tok, decrChk, "method's decreases clause must be below or equal to that in the trait"));

+      builder.Add(Assert(original.Tok, decrChk, string.Format("{0}'s decreases clause must be below or equal to that in the trait", original.WhatKind)));

     }

 

     private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)

@@ -3738,7 +3728,7 @@ namespace Microsoft.Dafny {
         var typeParams = TrTypeParamDecls(f.TypeArgs);

         {

           var formals = new List<Variable>();

-          if (f.IsRecursive) {

+          if (f.IsFuelAware()) {

             formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true));

           }

           if (!f.IsStatic) {

@@ -3762,7 +3752,7 @@ namespace Microsoft.Dafny {
         List<Bpl.Expr> argsF = new List<Bpl.Expr>();

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

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

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           var sV = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));

           var s = new Bpl.IdentifierExpr(f.tok, sV);

           bvars.Add(sV);

@@ -3837,7 +3827,7 @@ namespace Microsoft.Dafny {
         var f1args = new List<Bpl.Expr>(tyexprs);

         var f0argsCanCall = new List<Bpl.Expr>(tyexprs);

         var f1argsCanCall = new List<Bpl.Expr>(tyexprs);

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s);

           bvars.Add(sV);

           f0args.Add(s); f1args.Add(s);  // but don't add to f0argsCanCall or f1argsCanCall

@@ -4079,8 +4069,8 @@ namespace Microsoft.Dafny {
         foreach (var p in GetTypeParams(f)) {

           args.Add(trTypeParam(p, null));

         }

-        if (f.IsRecursive) {

-          args.Add(etran.LayerN(1));

+        if (f.IsFuelAware()) {

+          args.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

         args.Add(etran.HeapExpr);

         if (!f.IsStatic) {

@@ -4113,8 +4103,8 @@ namespace Microsoft.Dafny {
         foreach (var p in GetTypeParams(f)) {

           args.Add(trTypeParam(p, null));

         }

-        if (f.IsRecursive) {

-          args.Add(etran.LayerN(1));

+        if (f.IsFuelAware()) {

+          args.Add(etran.layerInterCluster.GetFunctionFuel(f));

         }

         args.Add(etran.HeapExpr);

         foreach (Variable p in implInParams) {

@@ -5595,7 +5585,7 @@ namespace Microsoft.Dafny {
           tyargs.Add(TypeToTy(fm.Type));

         }

         tyargs.Add(TypeToTy(f.ResultType));

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           Bpl.Expr ly; vars.Add(BplBoundVar("$ly", predef.LayerType, out ly)); args.Add(ly);

           formals.Add(BplFormalVar(null, predef.LayerType, true));

         }

@@ -5655,7 +5645,6 @@ namespace Microsoft.Dafny {
         {

           // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)

           //   = F#Requires(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN)

-          //   || Scramble(...)

 

           var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(args));

           var lhs = FunctionCall(f.tok, Requires(arity), Bpl.Type.Bool, Concat(tyargs, Cons(fhandle, Cons(h, lhs_args))));

@@ -5664,9 +5653,7 @@ namespace Microsoft.Dafny {
             // In case this is the /requires/ or /reads/ function, then there is no precondition

             rhs = Bpl.Expr.True;

           } else {

-            rhs = BplOr(

-              FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, Concat(SnocSelf(Snoc(args, h)), rhs_args)),

-              MakeScrambler(f.tok, f.FullSanitizedName + "#lessReq", Concat(vars, bvars)));

+            rhs = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, Concat(SnocSelf(Snoc(args, h)), rhs_args));

           }

 

           sink.AddTopLevelDeclaration(new Axiom(f.tok,

@@ -5694,15 +5681,6 @@ namespace Microsoft.Dafny {
       return name;

     }

 

-    public Bpl.Expr MakeScrambler(IToken tk, string name, List<Variable> bvars) {

-      var f = new Bpl.Function(tk, name,

-        bvars.ConvertAll(bv => (Bpl.Variable)BplFormalVar(null, bv.TypedIdent.Type, true)),

-        BplFormalVar(null, Bpl.Type.Bool, false));

-

-      sink.AddTopLevelDeclaration(f);

-      return FunctionCall(tk, name, Bpl.Type.Bool, bvars.ConvertAll(bv => (Bpl.Expr)new Bpl.IdentifierExpr(tk, bv)));

-    }

-

     private void AddArrowTypeAxioms(ArrowTypeDecl ad) {

       Contract.Requires(ad != null);

       var arity = ad.Arity;

@@ -5748,11 +5726,9 @@ namespace Microsoft.Dafny {
 

       {

         // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box

-        //      :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN]

-        //

-        // no precondition for these, but:

-        // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN]

-        // for reads, we could:  ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't

+        //      :: ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == h[heap, b1, ..., bN]

+        //      :: RequiresN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) <== r[heap, b1, ..., bN]

+        //      :: ReadsN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == rd[heap, b1, ..., bN]

         Action<string, Bpl.Type, string, Bpl.Type, string, Bpl.Type> SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => {

           Contract.Assert((precond == null) == (precondTy == null));

           var bvars = new List<Bpl.Variable>();

@@ -5954,7 +5930,7 @@ namespace Microsoft.Dafny {
       var inner_name = GetClass(td).TypedIdent.Name;

       string name = "T" + inner_name;

       // Create the type constructor

-      {

+      if (td.Name != "object") {  // the type constructor for "object" is in DafnyPrelude.bpl

         Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false);

         List<Bpl.Variable> args = new List<Bpl.Variable>(

           Enumerable.Range(0, arity).Select(i =>

@@ -6160,7 +6136,7 @@ namespace Microsoft.Dafny {
         var typeParams = TrTypeParamDecls(f.TypeArgs);

         var formals = new List<Variable>();

         formals.AddRange(MkTyParamFormals(GetTypeParams(f)));

-        if (f.IsRecursive) {

+        if (f.IsFuelAware()) {

           formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true));

         }

         formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true));

@@ -6271,9 +6247,7 @@ namespace Microsoft.Dafny {
           } else {

             bool splitHappened;  // we actually don't care

             foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true /* kind == MethodTranslationKind.Implementation */, out splitHappened)) {

-              if ((kind == MethodTranslationKind.IntraModuleCall || kind == MethodTranslationKind.CoCall) && RefinementToken.IsInherited(s.E.tok, currentModule)) {

-                // this precondition was inherited into this module, so just ignore it

-              } else if (s.IsOnlyChecked && bodyKind) {

+              if (s.IsOnlyChecked && bodyKind) {

                 // don't include in split

               } else if (s.IsOnlyFree && !bodyKind) {

                 // don't include in split -- it would be ignored, anyhow

@@ -6520,7 +6494,7 @@ namespace Microsoft.Dafny {
       // parameters of the procedure

       List<Variable> inParams = new List<Variable>();

       Bpl.Formal layer;

-      if (f.IsRecursive) {

+      if (f.IsFuelAware()) {

         layer = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true);

         inParams.Add(layer);

       } else {

@@ -7043,7 +7017,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

       Contract.Requires(codeContext != null && predef != null);

+      Contract.Ensures(fuelContext == Contract.OldValue(fuelContext));

       if (stmt is PredicateStmt) {

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) {

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

           PredicateStmt s = (PredicateStmt)stmt;

@@ -7072,6 +7048,7 @@ namespace Microsoft.Dafny {
           TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

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

         }

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is PrintStmt) {

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

         PrintStmt s = (PrintStmt)stmt;

@@ -7304,6 +7281,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is WhileStmt) {

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

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         var s = (WhileStmt)stmt;

         BodyTranslator bodyTr = null;

         if (s.Body != null) {

@@ -7314,7 +7292,7 @@ namespace Microsoft.Dafny {
           };

         }

         TrLoop(s, s.Guard, bodyTr, builder, locals, etran);

-

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is AlternativeLoopStmt) {

         AddComment(builder, stmt, "alternative loop statement");

         var s = (AlternativeLoopStmt)stmt;

@@ -7356,6 +7334,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is ForallStmt) {

         var s = (ForallStmt)stmt;

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         if (s.Kind == ForallStmt.ParBodyKind.Assign) {

           AddComment(builder, stmt, "forall statement (assign)");

           Contract.Assert(s.Ens.Count == 0);

@@ -7399,7 +7378,7 @@ namespace Microsoft.Dafny {
         } else {

           Contract.Assert(false);  // unexpected kind

         }

-

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is CalcStmt) {

         /* Translate into:

         if (*) {

@@ -7425,6 +7404,7 @@ namespace Microsoft.Dafny {
         var s = (CalcStmt)stmt;

         Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver

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

+        this.fuelContext = FuelSetting.ExpandFuelContext(stmt.Attributes, this.fuelContext);

         CurrentIdGenerator.Push();  // put the entire calc statement within its own sub-branch

         if (s.Lines.Count > 0) {

           Bpl.IfCmd ifCmd = null;

@@ -7489,7 +7469,7 @@ namespace Microsoft.Dafny {
           }

         }

         CurrentIdGenerator.Pop();

-

+        this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);

@@ -10298,6 +10278,227 @@ namespace Microsoft.Dafny {
       }

     }

 

+    internal class FuelSettingPair 

+    {

+      public int low;

+      public int high;

+

+      public FuelSettingPair(int low = (int)FuelSetting.FuelAmount.LOW, int high = (int)FuelSetting.FuelAmount.HIGH) {

+        this.low = low;

+        this.high = high;

+      }

+    }

+

+    // C#'s version of a type alias

+    internal class FuelContext : Dictionary<Function, FuelSettingPair> { }

+

+    internal class FuelSetting

+    {

+      public enum FuelAmount { NONE, LOW, HIGH };

+      public static Stack<FuelContext> SavedContexts = new Stack<FuelContext>();

+

+      private static FuelSettingPair FuelAttrib(Function f) {

+        Contract.Requires(f != null);

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

+        FuelSettingPair setting = new FuelSettingPair();

+

+        if (f.Attributes != null) {

+          List<Expression> args = Attributes.FindExpressions(f.Attributes, "fuel");

+          if (args != null && args.Count >= 2) {

+            LiteralExpr literalLow = args[0] as LiteralExpr;

+            LiteralExpr literalHigh = args[1] as LiteralExpr;

+

+            if (literalLow != null && literalLow.Value is BigInteger && literalHigh != null && literalHigh.Value is BigInteger) {

+              setting.low = (int)((BigInteger)literalLow.Value);

+              setting.high = (int)((BigInteger)literalHigh.Value);

+            }

+          } else if (args != null && args.Count >= 1) {

+            LiteralExpr literal = args[0] as LiteralExpr;

+            if (literal != null && literal.Value is BigInteger) {

+              setting.low = (int)((BigInteger)literal.Value);

+              setting.high = setting.low + 1;

+            }

+          }

+        }

+

+        return setting;

+      }

+

+      public int amount;        // Amount of fuel above that represented by start

+      private Bpl.Expr start;   // Starting fuel argument (null indicates LZ)      

+      private Translator translator;

+

+      public FuelSetting(Translator translator, int amount, Bpl.Expr start = null) {

+        this.translator = translator;

+        this.amount = amount;

+        this.start = start;

+      }

+

+      public FuelSetting Offset(int offset) {

+        return new FuelSetting(translator, this.amount + offset, start);

+      }

+

+      public Bpl.Expr LayerZero() {

+        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+        return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", translator.predef.LayerType);

+      }

+

+      public Bpl.Expr LayerN(int n) {

+        Contract.Requires(0 <= n);

+        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+        return translator.LayerSucc(LayerZero(), n);

+      }

+

+      private Bpl.Expr ToExpr(int amount) {

+        if (start == null) {

+          return LayerN(amount);

+        } else {

+          return translator.LayerSucc(start, amount);

+        }

+      }

+

+      public Bpl.Expr ToExpr() {

+        return this.ToExpr(this.amount);

+      }

+

+      /// <summary>

+      /// Get the fuel value for this function, given the ambient environment (represented by the fuel setting)

+      /// the function itself, and the function call's context (if any)

+      /// </summary>      

+      public Bpl.Expr GetFunctionFuel(Function f) {

+        Contract.Requires(f != null);

+        if (this.amount == (int)FuelAmount.NONE) {

+          return this.ToExpr();

+        } else {

+          FuelSettingPair setting = null;

+          var found = translator.fuelContext.TryGetValue(f, out setting);

+

+          if (!found) {  // If the context doesn't define fuel for this function, check for a fuel attribute (which supplies a default value if none is found)

+            setting = FuelAttrib(f);

+          }

+

+          if (this.amount == (int)FuelAmount.LOW) {

+            return ToExpr(setting.low);

+          } else if (this.amount == (int)FuelAmount.HIGH) {

+            return ToExpr(setting.high);

+          } else {

+            Contract.Assert(false); // Should not reach here

+            return null;

+          }

+        }

+      }

+

+

+      /// <summary>

+      /// Finds all fuel related attributes of the form {:fuel function low [high]}

+      /// Adds the setting to the context _if_ the context does not already have a setting for that function.

+      /// In other words, it should be called in order from most to least specific contenxt scope.

+      /// </summary>    

+      private static void FindFuelAttributes(Attributes attribs, FuelContext fuelContext) {

+        Function f = null;

+        FuelSettingPair setting = null;

+

+        if (attribs != null) {

+          List<List<Expression>> results = Attributes.FindAllExpressions(attribs, "fuel");

+

+          if (results != null) {

+            foreach (List<Expression> args in results) {

+              if (args != null && args.Count >= 2) {

+                // Try to extract the function from the first argument

+                MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr;

+                if (selectExpr != null) {

+                  f = selectExpr.Member as Function;

+                }

+

+                // Try to extract the lower fuel setting

+                LiteralExpr literalLow = args[1] as LiteralExpr;

+                if (literalLow != null && literalLow.Value is BigInteger) {

+                  setting = new FuelSettingPair();

+                  setting.low = (int)((BigInteger)literalLow.Value);

+                }

+

+                // The user may supply an additional high argument; if not, it defaults to low + 1

+                if (f != null && args.Count >= 3) {

+                  LiteralExpr literalHigh = args[2] as LiteralExpr;

+                  if (setting != null && literalHigh != null && literalHigh.Value is BigInteger) {

+                    setting.high = (int)((BigInteger)literalHigh.Value);

+                    if (!fuelContext.ContainsKey(f)) {

+                      fuelContext.Add(f, setting);

+                    }

+                  }

+                } else if (f != null && setting != null) {

+                  setting.high = setting.low + 1;

+                  if (!fuelContext.ContainsKey(f)) {

+                    fuelContext.Add(f, setting);

+                  }

+                }

+              }

+            }

+          }

+        }

+      }

+

+      /// <summary>

+      /// Extend the given context with fuel information from the declaration itself, and enclosing modules

+      /// </summary>

+      private static void AddFuelContext(FuelContext context, TopLevelDecl decl) {

+        FindFuelAttributes(decl.Attributes, context);

+

+        var module = decl.Module;

+        while (module != null) {

+          FindFuelAttributes(module.Attributes, context);

+          module = module.Module;

+        }

+      }

+

+      /// <summary>

+      /// Creates a summary of all fuel settings in scope, starting from the given class declaration

+      /// </summary>      

+      public static FuelContext NewFuelContext(TopLevelDecl decl) {

+        FuelContext context = new FuelContext();

+        AddFuelContext(context, decl);

+        return context;

+      }

+

+      /// <summary>

+      /// Creates a summary of all fuel settings in scope, starting from the given member declaration      

+      /// </summary>      

+      public static FuelContext NewFuelContext(MemberDecl decl) {

+        FuelContext context = new FuelContext();

+

+        FindFuelAttributes(decl.Attributes, context);

+        AddFuelContext(context, decl.EnclosingClass);

+        

+        return context;

+      }

+

+      /// <summary>

+      /// Extends the given fuel context with any new fuel settings found in attribs

+      /// </summary>    

+      public static FuelContext ExpandFuelContext(Attributes attribs, FuelContext oldFuelContext) {

+        Contract.Ensures(SavedContexts.Count == Contract.OldValue(SavedContexts.Count) + 1);

+        FuelContext newContext = new FuelContext();

+        FindFuelAttributes(attribs, newContext);

+        if (newContext.Count > 0) {

+          foreach (var pair in oldFuelContext) {

+            if (!newContext.ContainsKey(pair.Key)) {    // Local setting takes precedence over old context

+              newContext.Add(pair.Key, pair.Value);              

+            }

+          }          

+        } else {

+          newContext = oldFuelContext;

+        }

+        SavedContexts.Push(oldFuelContext);

+        return newContext;

+      }

+

+      public static FuelContext PopFuelContext() {

+        Contract.Requires(SavedContexts.Count > 0);

+        return SavedContexts.Pop();

+      }

+

+    }

+

     internal class ExpressionTranslator

     {

       public readonly Bpl.Expr HeapExpr;

@@ -10306,8 +10507,8 @@ namespace Microsoft.Dafny {
       public readonly string This;

       public readonly string modifiesFrame; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

-      public readonly Bpl.Expr layerInterCluster;

-      public readonly Bpl.Expr layerIntraCluster = null;  // a value of null says to do the same as for inter-cluster calls

+      public readonly FuelSetting layerInterCluster;

+      public readonly FuelSetting layerIntraCluster = null;  // a value of null says to do the same as for inter-cluster calls

       public int Statistics_CustomLayerFunctionCount = 0;

       public readonly bool ProducingCoCertificates = false; // CLEMENT Where is this used?

       public readonly bool stripLits = false;

@@ -10325,41 +10526,16 @@ namespace Microsoft.Dafny {
       }

 

       /// <summary>

-      /// This is a general constructor, but takes the layerInterCluster as an int.

-      /// </summary>

-      ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

-        Function applyLimited_CurrentFunction, int layerInterCluster, Bpl.Expr layerIntraCluster, string modifiesFrame, bool stripLits) {

-

-        Contract.Requires(translator != null);

-        Contract.Requires(predef != null);

-        Contract.Requires(heap != null);

-        Contract.Requires(thisVar != null);

-        Contract.Requires(0 <= layerInterCluster);

-        Contract.Requires(modifiesFrame != null);

-

-        this.translator = translator;

-        this.predef = predef;

-        this.HeapExpr = heap;

-        this.This = thisVar;

-        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;

-        this.layerInterCluster = LayerN(layerInterCluster);

-        this.layerIntraCluster = layerIntraCluster;

-        this.modifiesFrame = modifiesFrame;

-        this.stripLits = stripLits;

-      }

-

-      /// <summary>

       /// This is the most general constructor.  It is private and takes all the parameters.  Whenever

       /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.

       /// </summary>

       ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,

-        Function applyLimited_CurrentFunction, Bpl.Expr layerInterCluster, Bpl.Expr layerIntraCluster, string modifiesFrame, bool stripLits) {

+        Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string modifiesFrame, bool stripLits) {

 

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

         Contract.Requires(heap != null);

-        Contract.Requires(thisVar != null);

-        Contract.Requires(layerInterCluster != null);

+        Contract.Requires(thisVar != null);       

         Contract.Requires(modifiesFrame != null);

 

         this.translator = translator;

@@ -10404,7 +10580,7 @@ namespace Microsoft.Dafny {
       }

 

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar)

-        : this(translator, predef, heap, thisVar, null, 1, null, "$_Frame", false) {

+        : this(translator, predef, heap, thisVar, null, new FuelSetting(translator, 1), null, "$_Frame", false) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

         Contract.Requires(heap != null);

@@ -10448,9 +10624,9 @@ namespace Microsoft.Dafny {
         Contract.Requires(layerArgument != null);

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

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, This, null, layerArgument, layerArgument, modifiesFrame, stripLits);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, null, new FuelSetting(translator, 0, layerArgument), new FuelSetting(translator, 0, layerArgument), modifiesFrame, stripLits);

       }

-

+      

       public ExpressionTranslator WithNoLits() {

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

         return new ExpressionTranslator(translator, predef, HeapExpr, This, null, layerInterCluster, layerIntraCluster, modifiesFrame, true);

@@ -10461,16 +10637,16 @@ namespace Microsoft.Dafny {
         Contract.Requires(layerArgument != null);

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

 

-        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, /* layerArgument */ layerInterCluster, layerArgument, modifiesFrame, stripLits);

+        return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, /* layerArgument */ layerInterCluster, new FuelSetting(translator, 0, layerArgument), modifiesFrame, stripLits);

       }

 

       public ExpressionTranslator LayerOffset(int offset) {

         Contract.Requires(0 <= offset);

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

 

-        var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, translator.LayerSucc(layerInterCluster, offset), layerIntraCluster, modifiesFrame, stripLits);

+        var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Offset(offset), layerIntraCluster, modifiesFrame, stripLits);

         if (this.oldEtran != null) {

-          var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, translator.LayerSucc(layerInterCluster, offset), layerIntraCluster, modifiesFrame, stripLits);

+          var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster.Offset(offset), layerIntraCluster, modifiesFrame, stripLits);

           etOld.oldEtran = etOld;

           et.oldEtran = etOld;

         }

@@ -10509,17 +10685,6 @@ namespace Microsoft.Dafny {
         }

       }

 

-      public Bpl.Expr LayerZero() {

-        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

-        return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", predef.LayerType);

-      }

-

-      public Bpl.Expr LayerN(int n) {

-        Contract.Requires(0 <= n);

-        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

-        return translator.LayerSucc(LayerZero(), n);

-      }

-

       public Bpl.IdentifierExpr ModuleContextHeight() {

         Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);

         return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);

@@ -10701,8 +10866,8 @@ namespace Microsoft.Dafny {
             },

             fn => {

               var args = e.TypeApplication.ConvertAll(translator.TypeToTy);

-              if (fn.IsRecursive) {

-                args.Add(layerInterCluster);

+              if (fn.IsFuelAware()) {

+                args.Add(this.layerInterCluster.GetFunctionFuel(fn));

               }

               if (!fn.IsStatic) {

                 args.Add(/* translator.BoxIfUnboxed */(TrExpr(e.Obj)/*, e.Type */));

@@ -10858,15 +11023,15 @@ namespace Microsoft.Dafny {
         } else if (expr is FunctionCallExpr) {

           FunctionCallExpr e = (FunctionCallExpr)expr;

           Bpl.Expr layerArgument;

-          if (e.Function.IsRecursive) {

+          if (e.Function.IsFuelAware()) {

             Statistics_CustomLayerFunctionCount++;

             ModuleDefinition module = e.Function.EnclosingClass.Module;

             if (this.applyLimited_CurrentFunction != null &&

               this.layerIntraCluster != null &&

               ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) {

-              layerArgument = this.layerIntraCluster;

+              layerArgument = this.layerIntraCluster.GetFunctionFuel(e.Function);

             } else {

-              layerArgument = this.layerInterCluster;

+              layerArgument = this.layerInterCluster.GetFunctionFuel(e.Function);

             }

           } else {

             layerArgument = null;

@@ -10941,6 +11106,7 @@ namespace Microsoft.Dafny {
               var eeType = e.E.Type.NormalizeExpand();

               if (eeType is SetType) {

                 // generate:  (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])

+                // TODO: trigger?

                 Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));

                 Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);

                 Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);

@@ -10967,7 +11133,7 @@ namespace Microsoft.Dafny {
                 //TRIGGERS: Does this make sense? dafny0\SmallTests

                 // BROKEN // NEW_TRIGGER

                 //TRIG (forall $i: int :: 0 <= $i && $i < Seq#Length(Q#0) && $Unbox(Seq#Index(Q#0, $i)): ref != null ==> !read(old($Heap), $Unbox(Seq#Index(Q#0, $i)): ref, alloc))

-                return new Bpl.ForallExpr(expr.tok, new List<Variable> { iVar }, body); 

+                return new Bpl.ForallExpr(expr.tok, new List<Variable> { iVar }, body);

               } else if (eeType.IsDatatype) {

                 // translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr);

                 Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), eeType, Old.HeapExpr);

@@ -11051,7 +11217,7 @@ namespace Microsoft.Dafny {
               if (cot != null) {

                 var e0args = e.E0.Type.NormalizeExpand().TypeArgs;

                 var e1args = e.E1.Type.NormalizeExpand().TypeArgs;

-                return translator.CoEqualCall(cot, e0args, e1args, null, LayerN(2), e0, e1, expr.tok);

+                return translator.CoEqualCall(cot, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, expr.tok);

               }

               typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Eq; break;

@@ -11060,7 +11226,7 @@ namespace Microsoft.Dafny {
               if (cotx != null) {

                 var e0args = e.E0.Type.NormalizeExpand().TypeArgs;

                 var e1args = e.E1.Type.NormalizeExpand().TypeArgs;

-                var x = translator.CoEqualCall(cotx, e0args, e1args, null, LayerN(2), e0, e1, expr.tok);

+                var x = translator.CoEqualCall(cotx, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, expr.tok);

                 return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, x);

               }

               typ = Bpl.Type.Bool;

@@ -11341,7 +11507,7 @@ namespace Microsoft.Dafny {
               var e2type = e.E2.Type.NormalizeExpand();

               var cot = e1type.AsCoDatatype;

               Contract.Assert(cot != null);  // the argument types of prefix equality (and prefix disequality) are codatatypes

-              var r = translator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, LayerN(2), e1, e2);

+              var r = translator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e1, e2);

               if (e.Op == TernaryExpr.Opcode.PrefixEqOp) {

                 return r;

               } else {

@@ -11374,8 +11540,7 @@ namespace Microsoft.Dafny {
           if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) {

             // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body

             var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars);

-            Expr layer = translator.LayerSucc(ly);

-            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layer, layer, modifiesFrame, stripLits);

+            bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits);

           }

           if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) {

             var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars);

@@ -11496,7 +11661,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

         }

       }

-      

+

       private Expr TrLambdaExpr(LambdaExpr e) {

         var bvars = new List<Bpl.Variable>();

         var bargs = new List<Bpl.Expr>();

@@ -11534,13 +11699,10 @@ namespace Microsoft.Dafny {
         }

 

         var rdvars = new List<Bpl.Variable>();

-        var o = translator.UnboxIfBoxed(BplBoundVar(varNameGen.FreshId("#o#"), predef.BoxType, rdvars), new ObjectType());

-

-        Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), et.IsAlloced(e.tok, o));

-        Bpl.Expr consequent = translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null);

-        Bpl.Expr rdbody =

-          new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,

-            BplImp(ante, consequent));

+        var o = BplBoundVar(varNameGen.FreshId("#o#"), predef.RefType, rdvars);

+        Bpl.Expr rdbody = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,

+          translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null));

+        rdbody = translator.FunctionCall(e.tok, "SetRef_to_SetBox", predef.SetType(e.tok, true, predef.BoxType), rdbody);

 

         return MaybeLit(

           translator.FunctionCall(e.tok, BuiltinFunction.AtLayer, predef.HandleType,

@@ -11549,7 +11711,7 @@ namespace Microsoft.Dafny {
                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, ebody),

                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, reqbody),

                 new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), bvars, null, rdbody))),

-            layerIntraCluster ?? layerInterCluster),

+                layerIntraCluster != null ? layerIntraCluster.ToExpr() : layerInterCluster.ToExpr()),

           predef.HandleType);

       }

 

@@ -12641,15 +12803,14 @@ namespace Microsoft.Dafny {
           //   checked $PrefixEqual#Dt(k, A, B) || (0 < k ==> A.Cons? ==> B.Cons? && A.head == B.head && $PrefixEqual#2#Dt(k - 1, A.tail, B.tail))  // note the #2 in the recursive call, just like for user-defined predicates that are inlined by TrSplitExpr

           //   free $PrefixEqual#Dt(k, A, B);

           var kPos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);

-          var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, k, etran.LayerN(2), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);

+          var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, k, etran.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);

           var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));

           // for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions)

           var etran2 = etran.LayerOffset(1);

           var A2 = etran2.TrExpr(e.E1);

           var B2 = etran2.TrExpr(e.E2);

           var needsTokenAdjust = TrSplitNeedsTokenAdjustment(expr);

-          // Dan: dafny4/Circ.dfy needs this one to be 2+, rather than 1+

-          Bpl.Expr layer = LayerSucc(etran.layerInterCluster, 2);

+          Bpl.Expr layer = etran.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH);

           foreach (var c in CoPrefixEquality(needsTokenAdjust ? new ForceCheckToken(expr.tok) : expr.tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) {

             var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kPos, c));

             splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));

@@ -14061,7 +14222,7 @@ namespace Microsoft.Dafny {
           r = rr;

         } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          var rr = new CalcStmt(s.Tok, s.EndTok, SubstCalcOp(s.Op), s.Lines.ConvertAll(Substitute), s.Hints.ConvertAll(SubstBlockStmt), s.StepOps.ConvertAll(SubstCalcOp), SubstCalcOp(s.ResultOp));

+          var rr = new CalcStmt(s.Tok, s.EndTok, SubstCalcOp(s.Op), s.Lines.ConvertAll(Substitute), s.Hints.ConvertAll(SubstBlockStmt), s.StepOps.ConvertAll(SubstCalcOp), SubstCalcOp(s.ResultOp), SubstAttributes(s.Attributes));

           rr.Steps.AddRange(s.Steps.ConvertAll(Substitute));

           rr.Result = Substitute(s.Result);

           r = rr;

@@ -14352,7 +14513,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(b != null);

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

 

-      if (a == Bpl.Expr.True || b == Bpl.Expr.True || b == Bpl.Expr.False) {

+      if (a == Bpl.Expr.True || b == Bpl.Expr.True) {

         return b;

       } else if (a == Bpl.Expr.False) {

         return Bpl.Expr.True;

@@ -14384,7 +14545,7 @@ namespace Microsoft.Dafny {
 

     /// Makes a simple trigger

     static Bpl.Trigger BplTrigger(Bpl.Expr e) {

-      return new Trigger(e.tok, true, new List<Bpl.Expr> { e });

+      return new Bpl.Trigger(e.tok, true, new List<Bpl.Expr> { e });

     }

 

     static Bpl.Axiom BplAxiom(Bpl.Expr e) {