Fix issue 75. Adjust the fuel for existentials to use more fuel in an assume

context and less in an assert.

5 files changed, 169 insertions, 72 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0e4c4751..ab1a411a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2375,6 +2375,7 @@ namespace Microsoft.Dafny {
     bool MustReverify { get; }

     string FullSanitizedName { get; }

     bool AllowsNontermination { get; }

+    bool ContainsQuantifier { get;  set; }

   }

   /// <summary>

   /// An ICallable is a Function, Method, IteratorDecl, or RedirectingTypeDecl.

@@ -2392,6 +2393,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     bool InferredDecreases { get; set; }

   }

+

   public class DontUseICallable : ICallable

   {

     public string WhatKind { get { throw new cce.UnreachableException(); } }

@@ -2409,6 +2411,10 @@ namespace Microsoft.Dafny {
       get { throw new cce.UnreachableException(); }

       set { throw new cce.UnreachableException(); }

     }

+    public bool ContainsQuantifier {

+      get { throw new cce.UnreachableException(); }

+      set { throw new cce.UnreachableException(); }

+    }

   }

   /// <summary>

   /// An IMethodCodeContext is a Method or IteratorDecl.

@@ -2437,6 +2443,11 @@ namespace Microsoft.Dafny {
     bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

     public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

     public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }

+    public bool ContainsQuantifier { 

+      get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); }

+      set { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); }

+    }

+    

   }

 

   public class IteratorDecl : ClassDecl, IMethodCodeContext

@@ -2464,6 +2475,8 @@ namespace Microsoft.Dafny {
     public Predicate Member_Valid;  // created during registration phase of resolution; its specification is filled in during resolution

     public Method Member_MoveNext;  // created during registration phase of resolution; its specification is filled in during resolution

     public readonly LocalVariable YieldCountVariable;

+    bool containsQuantifier;

+

     public IteratorDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

                         List<Formal> ins, List<Formal> outs,

                         Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> decreases,

@@ -2579,6 +2592,10 @@ namespace Microsoft.Dafny {
       set { _inferredDecr = value; }

       get { return _inferredDecr; }

     }

+    bool ICodeContext.ContainsQuantifier {

+      set { containsQuantifier = value; }

+      get { return containsQuantifier; }

+    }

     ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }

     bool ICodeContext.MustReverify { get { return false; } }

     public bool AllowsNontermination {

@@ -2832,7 +2849,10 @@ namespace Microsoft.Dafny {
       get { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases

       set { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases

     }

-

+    bool ICodeContext.ContainsQuantifier {

+      get { throw new cce.UnreachableException(); }

+      set { throw new cce.UnreachableException(); }

+    }

     public new NewtypeDecl ClonedFrom {

       get {

         return (NewtypeDecl)base.ClonedFrom;

@@ -2890,6 +2910,10 @@ namespace Microsoft.Dafny {
       get { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases

       set { throw new cce.UnreachableException(); }  // see comment above about ICallable.Decreases

     }

+    bool ICodeContext.ContainsQuantifier {

+      get { throw new cce.UnreachableException(); }

+      set { throw new cce.UnreachableException(); }

+    }

   }

 

   [ContractClass(typeof(IVariableContracts))]

@@ -3184,6 +3208,11 @@ namespace Microsoft.Dafny {
     public readonly IToken SignatureEllipsis;

     public bool IsBuiltin;

     public Function OverriddenFunction;

+    public bool containsQuantifier;

+    public bool ContainsQuantifier { 

+      set { containsQuantifier = value; }

+      get { return containsQuantifier;  }

+    }

 

     public override IEnumerable<Expression> SubExpressions {

       get {

@@ -3438,6 +3467,7 @@ namespace Microsoft.Dafny {
     public bool IsTailRecursive;  // filled in during resolution

     public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();

     public Method OverriddenMethod;

+    public bool containsQuantifier;

 

     public override IEnumerable<Expression> SubExpressions {

       get {

@@ -3512,6 +3542,11 @@ namespace Microsoft.Dafny {
       set { _inferredDecr = value; }

       get { return _inferredDecr; }

     }

+    bool ICodeContext.ContainsQuantifier {

+      set { containsQuantifier = value; }

+      get { return containsQuantifier; }

+    }

+

     ModuleDefinition ICodeContext.EnclosingModule {

       get {

         Contract.Assert(this.EnclosingClass != null);  // this getter is supposed to be called only after signature-resolution is complete

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index aa9ce148..b6e783b4 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8173,6 +8173,7 @@ namespace Microsoft.Dafny
         e.Type = e.Body.Type;

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

+        opts.codeContext.ContainsQuantifier = true;

         Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

         bool _val = true;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9466f18a..b2b63a07 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7232,7 +7232,9 @@ namespace Microsoft.Dafny {
           AddComment(builder, stmt, "assume statement");

           AssumeStmt s = (AssumeStmt)stmt;

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

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

+          // we need to increase fuel for quantifier expr and functions that contain quantifier expr in the assume context.

+          var existEtran = etran.LayerOffset(1);

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

         }

         this.fuelContext = FuelSetting.PopFuelContext();

       } else if (stmt is PrintStmt) {

@@ -8348,7 +8350,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);

+            qq = callEtran.TrExpr(p, initEtran, null, null);

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

           }

         } else {

@@ -8485,7 +8487,7 @@ namespace Microsoft.Dafny {
 

       Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

       var p = Substitute(s.ForallExpressions[0], null, substMap);

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

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

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

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

       } else {

@@ -10916,9 +10918,9 @@ namespace Microsoft.Dafny {
       /// then show up in an error message).

       /// </summary>

       public Bpl.Expr TrExpr(Expression expr) {

-        return TrExpr(expr, null);

+        return TrExpr(expr, null, null, null);

       }

-      public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator etran)

+      public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator initEtran, ExpressionTranslator funcEtran, ExpressionTranslator existEtran)

       {

         Contract.Requires(expr != null);

         Contract.Requires(predef != null);

@@ -10982,7 +10984,7 @@ namespace Microsoft.Dafny {
             args.Add(Old.HeapExpr);

           }

           foreach (var arg in e.Args) {

-            args.Add(TrExpr(arg));

+            args.Add(TrExpr(arg, initEtran, funcEtran, existEtran));

           }

           return new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);

 

@@ -10990,7 +10992,7 @@ namespace Microsoft.Dafny {
           SetDisplayExpr e = (SetDisplayExpr)expr;

           Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.SetEmpty : BuiltinFunction.ISetEmpty, predef.BoxType);

           foreach (Expression ee in e.Elements) {

-            Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));

+            Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee, initEtran, funcEtran, existEtran), cce.NonNull(ee.Type));

             s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.SetUnionOne : BuiltinFunction.ISetUnionOne, predef.BoxType, s, ss);

           }

           return s;

@@ -10999,7 +11001,7 @@ namespace Microsoft.Dafny {
           MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;

           Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType);

           foreach (Expression ee in e.Elements) {

-            Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));

+            Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee, initEtran, funcEtran, existEtran), cce.NonNull(ee.Type));

             s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnionOne, predef.BoxType, s, ss);

           }

           return s;

@@ -11010,7 +11012,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);

           bool isLit = true;

           foreach (Expression ee in e.Elements) {

-            var rawElement = TrExpr(ee);

+            var rawElement = TrExpr(ee, initEtran, funcEtran, existEtran);

             isLit = isLit && translator.IsLit(rawElement);

             Bpl.Expr elt = BoxIfNecessary(expr.tok, rawElement, ee.Type);

             s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, elt);

@@ -11026,8 +11028,8 @@ namespace Microsoft.Dafny {
           Bpl.Type maptype = predef.MapType(expr.tok, e.Finite, predef.BoxType, predef.BoxType);

           Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.MapEmpty : BuiltinFunction.IMapEmpty, predef.BoxType);

           foreach (ExpressionPair p in e.Elements) {

-            Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A), cce.NonNull(p.A.Type));

-            Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B), cce.NonNull(p.B.Type));

+            Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A, initEtran, funcEtran, existEtran), cce.NonNull(p.A.Type));

+            Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B, initEtran, funcEtran, existEtran), cce.NonNull(p.B.Type));

             s = translator.FunctionCall(expr.tok, e.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2);

           }

           return s;

@@ -11036,7 +11038,7 @@ namespace Microsoft.Dafny {
           var e = (MemberSelectExpr)expr;

           return e.MemberSelectCase(

             field => {

-              Bpl.Expr obj = TrExpr(e.Obj);

+              Bpl.Expr obj = TrExpr(e.Obj, initEtran, funcEtran, existEtran);

               Bpl.Expr result;

               if (field.IsMutable) {

                 result = ReadHeap(expr.tok, HeapExpr, obj, new Bpl.IdentifierExpr(expr.tok, translator.GetField(field)));

@@ -11063,7 +11065,7 @@ namespace Microsoft.Dafny {
             });

         } else if (expr is SeqSelectExpr) {

           SeqSelectExpr e = (SeqSelectExpr)expr;

-          Bpl.Expr seq = TrExpr(e.Seq);

+          Bpl.Expr seq = TrExpr(e.Seq, initEtran, funcEtran, existEtran);

           var seqType = e.Seq.Type.NormalizeExpand();

           Type elmtType = null;

           Type domainType = null;

@@ -11083,14 +11085,14 @@ namespace Microsoft.Dafny {
           } else { Contract.Assert(false); }

           Bpl.Type elType = translator.TrType(elmtType);

           Bpl.Type dType = translator.TrType(domainType);

-          Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0);

-          Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1);

+          Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0, initEtran, funcEtran, existEtran);

+          Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1, initEtran, funcEtran, existEtran);

           if (e.SelectOne) {

             Contract.Assert(e1 == null);

             Bpl.Expr x;

             if (seqType.IsArrayType) {

               Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0);

-              x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName);

+              x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq, initEtran, funcEtran, existEtran), fieldName);

             } else if (seqType is SeqType) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);

             } else if (seqType is MapType) {

@@ -11099,7 +11101,7 @@ namespace Microsoft.Dafny {
               x = translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), seq);

               x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType));

             } else if (seqType is MultiSetType) {

-              x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType));

+              x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq, initEtran, funcEtran, existEtran), BoxIfNecessary(expr.tok, e0, domainType));

             } else { Contract.Assert(false); x = null; }

             if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) {

               x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);

@@ -11130,32 +11132,32 @@ namespace Microsoft.Dafny {
           SeqUpdateExpr e = (SeqUpdateExpr)expr;

           if (e.ResolvedUpdateExpr != null)

           {

-            return TrExpr(e.ResolvedUpdateExpr);

+            return TrExpr(e.ResolvedUpdateExpr, initEtran, funcEtran, existEtran);

           }

           else

           {

-            Bpl.Expr seq = TrExpr(e.Seq);

+            Bpl.Expr seq = TrExpr(e.Seq, initEtran, funcEtran, existEtran);

             var seqType = e.Seq.Type.NormalizeExpand();

             if (seqType is SeqType)

             {

               Type elmtType = cce.NonNull((SeqType)seqType).Arg;

-              Bpl.Expr index = TrExpr(e.Index);

-              Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);

+              Bpl.Expr index = TrExpr(e.Index, initEtran, funcEtran, existEtran);

+              Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value, initEtran, funcEtran, existEtran), elmtType);

               return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);

             }

             else if (seqType is MapType)

             {

               MapType mt = (MapType)seqType;

               Bpl.Type maptype = predef.MapType(expr.tok, mt.Finite, predef.BoxType, predef.BoxType);

-              Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain);

-              Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range);

+              Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index, initEtran, funcEtran, existEtran), mt.Domain);

+              Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value, initEtran, funcEtran, existEtran), mt.Range);

               return translator.FunctionCall(expr.tok, mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val);

             }

             else if (seqType is MultiSetType)

             {

               Type elmtType = cce.NonNull((MultiSetType)seqType).Arg;

-              Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType);

-              Bpl.Expr val = TrExpr(e.Value);

+              Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index, initEtran, funcEtran, existEtran), elmtType);

+              Bpl.Expr val = TrExpr(e.Value, initEtran, funcEtran, existEtran);

               return Bpl.Expr.StoreTok(expr.tok, seq, index, val);

             }

             else

@@ -11171,7 +11173,7 @@ namespace Microsoft.Dafny {
           Bpl.Type elType = translator.TrType(elmtType);

 

           Bpl.Expr fieldName = GetArrayIndexFieldName(expr.tok, e.Indices);

-          Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array), fieldName);

+          Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array, initEtran, funcEtran, existEtran), fieldName);

           if (!ModeledAsBoxType(elmtType)) {

             x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);

           }

@@ -11195,30 +11197,34 @@ namespace Microsoft.Dafny {
                 Function = fn,

                 Type = e.Type,

                 TypeArgumentSubstitutions = Util.Dict(GetTypeParams(fn), mem.TypeApplication)

-              });

+              }, initEtran, funcEtran, existEtran);

             }

           }

 

-          Func<Expression, Bpl.Expr> TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg), arg.Type);

+          Func<Expression, Bpl.Expr> TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg, initEtran, funcEtran, existEtran), arg.Type);

 

           var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType,

             Concat(Map(tt.TypeArgs,translator.TypeToTy),

-            Cons(TrExpr(e.Function), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));

+            Cons(TrExpr(e.Function, initEtran, funcEtran, existEtran), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg))))));

 

           return translator.UnboxIfBoxed(applied, tt.Result);

 

         } else if (expr is FunctionCallExpr) {

           FunctionCallExpr e = (FunctionCallExpr)expr;

           Bpl.Expr layerArgument;

+          var etran = this;

+          if (e.Function.ContainsQuantifier && funcEtran != null) {

+            etran = funcEtran;

+          } 

           if (e.Function.IsFuelAware()) {

             Statistics_CustomLayerFunctionCount++;

             ModuleDefinition module = e.Function.EnclosingClass.Module;

-            if (this.applyLimited_CurrentFunction != null &&

-              this.layerIntraCluster != null &&

+            if (etran.applyLimited_CurrentFunction != null &&

+              etran.layerIntraCluster != null &&

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

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

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

             } else {

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

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

             }

           } else {

             layerArgument = null;

@@ -11253,7 +11259,7 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < dtv.Arguments.Count; i++) {

             Expression arg = dtv.Arguments[i];

             Type t = dtv.Ctor.Formals[i].Type;

-            var bArg = TrExpr(arg);

+            var bArg = TrExpr(arg, initEtran, funcEtran, existEtran);

             argsAreLit = argsAreLit && translator.IsLit(bArg);

             args.Add(translator.CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t));

           }

@@ -11266,7 +11272,7 @@ namespace Microsoft.Dafny {
           return ret;

         } else if (expr is OldExpr) {

           OldExpr e = (OldExpr)expr;

-          return Old.TrExpr(e.E);

+          return Old.TrExpr(e.E, initEtran, funcEtran, existEtran);

 

         } else if (expr is MultiSetFormingExpr) {

           MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

@@ -11281,7 +11287,7 @@ namespace Microsoft.Dafny {
 

         } else if (expr is UnaryOpExpr) {

           var e = (UnaryOpExpr)expr;

-          Bpl.Expr arg = TrExpr(e.E);

+          Bpl.Expr arg = TrExpr(e.E, initEtran, funcEtran, existEtran);

           switch (e.Op) {

             case UnaryOpExpr.Opcode.Lit:

               return MaybeLit(arg);

@@ -11321,8 +11327,8 @@ namespace Microsoft.Dafny {
                 // generate:  (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc])

                 Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));

                 Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);

-                Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);

-                Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);

+                Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E, initEtran, funcEtran, existEtran), true, null, false);

+                Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E, initEtran, funcEtran, existEtran), i);

                 XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI);

                 Bpl.Expr oNotFresh = Old.IsAlloced(expr.tok, XsubI);

                 Bpl.Expr oIsFresh = Bpl.Expr.Not(oNotFresh);

@@ -11334,12 +11340,12 @@ namespace Microsoft.Dafny {
                 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);

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

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

               } else {

                 // generate:  x != null && !old($Heap)[x]

-                Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);

-                Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));

+                Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E, initEtran, funcEtran, existEtran), predef.Null);

+                Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E, initEtran, funcEtran, existEtran)));

                 return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And, oNull, oIsFresh);

               }

             default:

@@ -11359,14 +11365,14 @@ namespace Microsoft.Dafny {
             ct = BuiltinFunction.RealToInt;

           } else {

             Contract.Assert(fromInt == toInt);

-            return TrExpr(e.E);

+            return TrExpr(e.E, initEtran, funcEtran, existEtran);

           }

-          return translator.FunctionCall(e.tok, ct, null, TrExpr(e.E));

+          return translator.FunctionCall(e.tok, ct, null, TrExpr(e.E, initEtran, funcEtran, existEtran));

 

         } else if (expr is BinaryExpr) {

           BinaryExpr e = (BinaryExpr)expr;

           bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real);

-          Bpl.Expr e0 = TrExpr(e.E0);

+          Bpl.Expr e0 = TrExpr(e.E0, initEtran, funcEtran, existEtran);

           if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {

             return TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type));  // let TrInSet translate e.E1

           } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {

@@ -11378,7 +11384,7 @@ namespace Microsoft.Dafny {
             Bpl.Expr arg = TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type));  // let TrInMultiSet translate e.E1

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

           }

-          Bpl.Expr e1 = TrExpr(e.E1);

+          Bpl.Expr e1 = TrExpr(e.E1, initEtran, funcEtran, existEtran);

           BinaryOperator.Opcode bOpcode;

           Bpl.Type typ;

           var oe0 = e0;

@@ -11695,9 +11701,9 @@ namespace Microsoft.Dafny {
           return re;

         } else if (expr is TernaryExpr) {

           var e = (TernaryExpr)expr;

-          var e0 = TrExpr(e.E0);

-          var e1 = TrExpr(e.E1);

-          var e2 = TrExpr(e.E2);

+          var e0 = TrExpr(e.E0, initEtran, funcEtran, existEtran);

+          var e1 = TrExpr(e.E1, initEtran, funcEtran, existEtran);

+          var e2 = TrExpr(e.E2, initEtran, funcEtran, existEtran);

           switch (e.Op) {

             case TernaryExpr.Opcode.PrefixEqOp:

             case TernaryExpr.Opcode.PrefixNeqOp:

@@ -11717,24 +11723,25 @@ namespace Microsoft.Dafny {
         } else if (expr is LetExpr) {

           var e = (LetExpr)expr;

           if (e.Exact) {

-            return TrExpr(GetSubstitutedBody(e));

+            return TrExpr(GetSubstitutedBody(e), initEtran, funcEtran, existEtran);

           } else {

             var d = translator.LetDesugaring(e);

-            return TrExpr(d);

+            return TrExpr(d, initEtran, funcEtran, existEtran);

           }

         } else if (expr is NamedExpr) {

-          return TrExpr(((NamedExpr)expr).Body);

+          return TrExpr(((NamedExpr)expr).Body, initEtran, funcEtran, existEtran);

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

 

           if (e.SplitQuantifier != null) {

-            return TrExpr(e.SplitQuantifierExpression);

+            return TrExpr(e.SplitQuantifierExpression, initEtran, existEtran, existEtran);

           } else {

             List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);

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

 

-            var initEtran = (etran == null) ? this : etran;

+            var etran = initEtran ?? this;

             var bodyEtran = this;

+            existEtran = e is ForallExpr ? this : existEtran;

             bool _scratch = true;

 

             Bpl.Expr antecedent = Bpl.Expr.True;

@@ -11750,11 +11757,11 @@ namespace Microsoft.Dafny {
               antecedent = BplAnd(new List<Bpl.Expr> {

               antecedent,

               translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h),

-              translator.HeapSameOrSucc(initEtran.HeapExpr, h)

+              translator.HeapSameOrSucc(etran.HeapExpr, h)

             });

             }

 

-            antecedent = BplAnd(antecedent, initEtran.TrBoundVariables(e.BoundVars, bvars));

+            antecedent = BplAnd(antecedent, etran.TrBoundVariables(e.BoundVars, bvars));

 

             Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

             Bpl.Trigger tr = null;

@@ -11763,15 +11770,15 @@ namespace Microsoft.Dafny {
               if (aa.Name == "trigger") {

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

                 foreach (var arg in aa.Args) {

-                  tt.Add(argsEtran.TrExpr(arg));

+                  tt.Add(argsEtran.TrExpr(arg, initEtran, existEtran, existEtran));

                 }

                 tr = new Bpl.Trigger(expr.tok, true, tt, tr);

               }

             }

             if (e.Range != null) {

-              antecedent = BplAnd(antecedent, initEtran.TrExpr(e.Range));

+              antecedent = BplAnd(antecedent, etran.TrExpr(e.Range, initEtran, existEtran, existEtran));

             }

-            Bpl.Expr body = bodyEtran.TrExpr(e.Term);

+            Bpl.Expr body = bodyEtran.TrExpr(e.Term, initEtran, existEtran, existEtran);

 

             if (e is ForallExpr) {

               return new Bpl.ForallExpr(expr.tok, new List<TypeVariable>(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body));

@@ -11790,8 +11797,8 @@ namespace Microsoft.Dafny {
           var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.CurrentIdGenerator.FreshId("$y#"), predef.BoxType));

           Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);

 

-          var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));

-          var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range)), eq);

+          var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term, initEtran, funcEtran, existEtran), e.Term.Type));

+          var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range, initEtran, funcEtran, existEtran)), eq);

           var triggers = translator.TrTrigger(this, e.Attributes, e.tok);

           var exst = new Bpl.ExistsExpr(expr.tok, bvars, triggers, ebody);

 

@@ -11818,9 +11825,9 @@ namespace Microsoft.Dafny {
           Dictionary<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();

           subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type));

 

-          var ebody = BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(translator.Substitute(e.Range, null, subst)));

+          var ebody = BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(translator.Substitute(e.Range, null, subst), initEtran, funcEtran, existEtran));

           Bpl.Expr l1 = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, ebody);

-          ebody = TrExpr(translator.Substitute(e.Term, null, subst));

+          ebody = TrExpr(translator.Substitute(e.Term, null, subst), initEtran, funcEtran, existEtran);

           Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type));

 

           bool finite = e.Finite;

@@ -11833,31 +11840,31 @@ namespace Microsoft.Dafny {
 

         } else if (expr is StmtExpr) {

           var e = (StmtExpr)expr;

-          return TrExpr(e.E);

+          return TrExpr(e.E, initEtran, funcEtran, existEtran);

 

         } else if (expr is ITEExpr) {

           ITEExpr e = (ITEExpr)expr;

-          var g = translator.RemoveLit(TrExpr(e.Test));

-          var thn = translator.RemoveLit(TrExpr(e.Thn));

-          var els = translator.RemoveLit(TrExpr(e.Els));

+          var g = translator.RemoveLit(TrExpr(e.Test, initEtran, funcEtran, existEtran));

+          var thn = translator.RemoveLit(TrExpr(e.Thn, initEtran, funcEtran, existEtran));

+          var els = translator.RemoveLit(TrExpr(e.Els, initEtran, funcEtran, existEtran));

           return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new List<Bpl.Expr> { g, thn, els });

 

         } else if (expr is MatchExpr) {

           var e = (MatchExpr)expr;

           var ite = DesugarMatchExpr(e);

-          return TrExpr(ite);

+          return TrExpr(ite, initEtran, funcEtran, existEtran);

 

         } else if (expr is ConcreteSyntaxExpression) {

           var e = (ConcreteSyntaxExpression)expr;

-          return TrExpr(e.ResolvedExpression);

+          return TrExpr(e.ResolvedExpression, initEtran, funcEtran, existEtran);

 

         } else if (expr is BoxingCastExpr) {

           BoxingCastExpr e = (BoxingCastExpr)expr;

-          return translator.CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

+          return translator.CondApplyBox(e.tok, TrExpr(e.E, initEtran, funcEtran, existEtran), e.FromType, e.ToType);

 

         } else if (expr is UnboxingCastExpr) {

           UnboxingCastExpr e = (UnboxingCastExpr)expr;

-          return translator.CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

+          return translator.CondApplyUnbox(e.tok, TrExpr(e.E, initEtran, funcEtran, existEtran), e.FromType, e.ToType);

 

         } else {

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

@@ -13314,8 +13321,10 @@ namespace Microsoft.Dafny {
         translatedExpression = etran.TrExpr(expr);

         splitHappened = false;

       } else {

+        // for quantifierExpr, we don't want to increase fuel in assert context

+        var existEtran = etran;

         etran = etran.LayerOffset(1);

-        translatedExpression = etran.TrExpr(expr);

+        translatedExpression = etran.TrExpr(expr, null, etran, existEtran);

         splitHappened = etran.Statistics_CustomLayerFunctionCount != 0;  // return true if the LayerOffset(1) came into play

       }

       if (TrSplitNeedsTokenAdjustment(expr)) {

diff --git a/Test/dafny4/Bug75.dfy b/Test/dafny4/Bug75.dfy
new file mode 100644
index 00000000..37d35f77
--- /dev/null
+++ b/Test/dafny4/Bug75.dfy
@@ -0,0 +1,50 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate R1(x:int, y:int) { x > 0 ==> R2(x - 1) }

+predicate R2(x:int) { exists y :: R1(x, y) }

+

+lemma L1(x:int)

+{

+    assume R2(x);

+    assert exists y :: R1(x, y); // FAILS

+}

+

+lemma L2(x:int)

+    requires R2(x); // Oddly, adding this requires fixes the problem

+{

+    assume R2(x);

+    assert exists y :: R1(x, y); // SUCCEEDS

+}

+

+// this predicate says that the first "n" elements of "s"

+

+// are in strictly increasing order

+

+predicate method Increasing(s: seq<int>, n: nat)

+  requires n <= |s|

+{

+  n < 2 ||

+  (s[n-2] < s[n-1] && Increasing(s, n-1))

+} 

+

+method Extend(s: seq<int>, n: nat) returns (n': nat)

+  requires n < |s|

+  requires forall i :: 0 <= i < n ==> Increasing(s, i)

+  ensures n <= n' <= |s|

+  ensures forall j :: 0 <= j < n' ==> Increasing(s, j)

+{

+  if 2 <= n && s[n-2] < s[n-1] {

+    n' := n + 1;

+  } else {

+    n' := n;

+  }

+}

+

+function pred(i:int):int { i - 1 }

+predicate f(a:int, s:int)            { (a <= 0 || (exists s0 :: f(pred(a), s0))) }

+

+lemma Fuel1(a:int, s:int)

+{

+    assert  f(a, s) <==> (a <= 0 || (exists s0 :: f(pred(a), s0))); // FAILS

+}

diff --git a/Test/dafny4/Bug75.dfy.expect b/Test/dafny4/Bug75.dfy.expect
new file mode 100644
index 00000000..aeb37948
--- /dev/null
+++ b/Test/dafny4/Bug75.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 13 verified, 0 errors