In method and iterator specifications, inline top-level predicates (except

protected predicated in cross-module calls) like in other places.

4 files changed, 98 insertions, 80 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 7d3f570d..172005cc 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1466,13 +1466,15 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Returns true if the body of function "f" is available in module "context".

-    /// This happens when "f" has a body, "f" is not opaque, and either "f" is declared

-    /// in module "context" or "f" is not protected.

+    /// This happens when the following conditions all hold:

+    ///   - "f" has a body

+    ///   - "f" is not opaque

+    ///   - "f" is declared as protected, then "context" is the current module and parameter "revealProtectedBody" is passed in as "true".

     /// </summary>

-    static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context) {

+    static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, bool revealProtectedBody) {

       Contract.Requires(f != null);

       Contract.Requires(context != null);

-      return f.Body != null && !IsOpaqueFunction(f) && (f.EnclosingClass.Module == context || !f.IsProtected);

+      return f.Body != null && !IsOpaqueFunction(f) && (!f.IsProtected || (revealProtectedBody && f.EnclosingClass.Module == context));

     }

     static bool IsOpaqueFunction(Function f) {

       Contract.Requires(f != null);

@@ -1571,8 +1573,7 @@ namespace Microsoft.Dafny {
             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

             comment = null;

           } else {

-            bool splitHappened;  // we actually don't care

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

+            foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) {

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

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

               } else {

@@ -1589,8 +1590,7 @@ namespace Microsoft.Dafny {
             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));

             comment = null;

           } else {

-            bool splitHappened;  // we actually don't care

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

+            foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) {

               if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {

                 // this postcondition was inherited into this module, so just ignore it

               } else {

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

             var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);

             var splits = new List<SplitExprInfo>();

-            bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight,false, etran);

+            bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, false, etran);

             foreach (var s in splits)

             {

                 if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule))

@@ -3975,7 +3975,7 @@ namespace Microsoft.Dafny {
       foreach (Expression p in f.Ens) {

         var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f);

         var splits = new List<SplitExprInfo>();

-        bool splitHappened /*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, etran);

+        bool splitHappened /*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, true, etran);

         foreach (var s in splits) {

           if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) {

             ens.Add(Ensures(s.E.tok, false, s.E, null, null));

@@ -6233,8 +6233,7 @@ namespace Microsoft.Dafny {
             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

             comment = null;

           } 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)) {

+            foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) {

               if (s.IsOnlyChecked && bodyKind) {

                 // don't include in split

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

@@ -6254,8 +6253,7 @@ namespace Microsoft.Dafny {
           if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {

             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, null));

           } 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)) {

+            foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) {

               var post = s.E;

               if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {

                 // this postcondition was inherited into this module, so make it into the form "$_reverifyPost ==> s.E"

@@ -11115,7 +11113,7 @@ namespace Microsoft.Dafny {
           result = translator.CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type);

           

           bool callIsLit = argsAreLit 

-            && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule)

+            && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule, true)

             && !e.Function.Reads.Any(); // Function could depend on external values

           if (callIsLit) {

             result = MaybeLit(result, ty);

@@ -12754,18 +12752,20 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<List<SplitExprInfo>>() != null);

 

       var splits = new List<SplitExprInfo>();

-      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, apply_induction, etran);

+      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, true, apply_induction, etran);

       return splits;

     }

 

-    List<SplitExprInfo/*!*/>/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, int heightLimit, bool apply_induction, out bool splitHappened)

+    List<SplitExprInfo> TrSplitExprForMethodSpec(Expression expr, ExpressionTranslator etran, MethodTranslationKind kind)

     {

       Contract.Requires(expr != null);

       Contract.Requires(etran != null);

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

 

       var splits = new List<SplitExprInfo>();

-      splitHappened = TrSplitExpr(expr, splits, true, heightLimit, apply_induction, etran);

+      var apply_induction = true;/*kind == MethodTranslationKind.Implementation*/;

+      bool splitHappened;  // we don't actually care

+      splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, kind != MethodTranslationKind.InterModuleCall, apply_induction, etran);

       return splits;

     }

 

@@ -12795,7 +12795,7 @@ namespace Microsoft.Dafny {
     /// if its body is available in the current context and its height is less than "heightLimit" (if "heightLimit" is

     /// passed in as 0, then no functions will be inlined).

     /// </summary>

-    bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, bool apply_induction, ExpressionTranslator etran) {

+    bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, bool inlineProtectedFunctions, bool apply_induction, ExpressionTranslator etran) {

       Contract.Requires(expr != null);

       Contract.Requires(expr.Type.IsBoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type.IsBoolType));

       Contract.Requires(splits != null);

@@ -12804,7 +12804,7 @@ namespace Microsoft.Dafny {
       if (expr is BoxingCastExpr) {

         var bce = (BoxingCastExpr)expr;

         var ss = new List<SplitExprInfo>();

-        if (TrSplitExpr(bce.E, ss, position, heightLimit, apply_induction, etran)) {

+        if (TrSplitExpr(bce.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {

           foreach (var s in ss) {

             splits.Add(new SplitExprInfo(s.Kind, CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType)));

           }

@@ -12813,22 +12813,22 @@ namespace Microsoft.Dafny {
 

       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

-        return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, apply_induction, etran);

+        return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

 

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

         if (e.Exact) {

-          return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, apply_induction, etran);

+          return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

         } else {

           var d = LetDesugaring(e);

-          return TrSplitExpr(d, splits, position, heightLimit, apply_induction, etran);

+          return TrSplitExpr(d, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

         }

 

       } else if (expr is UnaryOpExpr) {

         var e = (UnaryOpExpr)expr;

         if (e.Op == UnaryOpExpr.Opcode.Not) {

           var ss = new List<SplitExprInfo>();

-          if (TrSplitExpr(e.E, ss, !position, heightLimit, apply_induction, etran)) {

+          if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {

             foreach (var s in ss) {

               splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));

             }

@@ -12839,13 +12839,13 @@ namespace Microsoft.Dafny {
       } else if (expr is BinaryExpr) {

         var bin = (BinaryExpr)expr;

         if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

-          TrSplitExpr(bin.E0, splits, position, heightLimit, apply_induction, etran);

-          TrSplitExpr(bin.E1, splits, position, heightLimit, apply_induction, etran);

+          TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

+          TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

           return true;

 

         } else  if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {

-          TrSplitExpr(bin.E0, splits, position, heightLimit, apply_induction, etran);

-          TrSplitExpr(bin.E1, splits, position, heightLimit, apply_induction, etran);

+          TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

+          TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

           return true;

 

         } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {

@@ -12853,14 +12853,14 @@ namespace Microsoft.Dafny {
           if (position) {

             var lhs = etran.TrExpr(bin.E0);

             var ss = new List<SplitExprInfo>();

-            TrSplitExpr(bin.E1, ss, position, heightLimit, apply_induction, etran);

+            TrSplitExpr(bin.E1, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

             foreach (var s in ss) {

               // as the source location in the following implication, use that of the translated "s"

               splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E)));

             }

           } else {

             var ss = new List<SplitExprInfo>();

-            TrSplitExpr(bin.E0, ss, !position, heightLimit, apply_induction, etran);

+            TrSplitExpr(bin.E0, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

             var rhs = etran.TrExpr(bin.E1);

             foreach (var s in ss) {

               // as the source location in the following implication, use that of the translated "s"

@@ -12907,8 +12907,8 @@ namespace Microsoft.Dafny {
         var ssThen = new List<SplitExprInfo>();

         var ssElse = new List<SplitExprInfo>();

 

-        TrSplitExpr(ite.Thn, ssThen, position, heightLimit, apply_induction, etran);

-        TrSplitExpr(ite.Els, ssElse, position, heightLimit, apply_induction, etran);

+        TrSplitExpr(ite.Thn, ssThen, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

+        TrSplitExpr(ite.Els, ssElse, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

 

         var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And;

         var test = etran.TrExpr(ite.Test);

@@ -12934,14 +12934,14 @@ namespace Microsoft.Dafny {
         if (position) {

           var conclusion = etran.TrExpr(e.GetSConclusion());

           var ss = new List<SplitExprInfo>();

-          TrSplitExpr(e.E, ss, position, heightLimit, apply_induction, etran);

+          TrSplitExpr(e.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

           foreach (var s in ss) {

             // as the source location in the following implication, use that of the translated "s"

             splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, conclusion, s.E)));

           }

         } else {

           var ss = new List<SplitExprInfo>();

-          TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, apply_induction, etran);

+          TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

           var rhs = etran.TrExpr(e.E);

           foreach (var s in ss) {

             // as the source location in the following implication, use that of the translated "s"

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

       } else if (expr is OldExpr) {

         var e = (OldExpr)expr;

-        return TrSplitExpr(e.E, splits, position, heightLimit, apply_induction, etran.Old);

+        return TrSplitExpr(e.E, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran.Old);

 

       } else if (expr is FunctionCallExpr && position) {

         var fexp = (FunctionCallExpr)expr;

@@ -12961,22 +12961,17 @@ namespace Microsoft.Dafny {
         var module = f.EnclosingClass.Module;

         var functionHeight = module.CallGraph.GetSCCRepresentativeId(f);

 

-        if (module == currentModule && functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) {

+        if (functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) {

           if (RefinementToken.IsInherited(fexp.tok, currentModule) &&

               f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&

               (codeContext == null || !codeContext.MustReverify)) {

             // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything

             // that needed to be proved about the function was proved already in the previous module, even without the body definition).

-          } else if (!FunctionBodyIsAvailable(f, currentModule)) {

+          } else if (!FunctionBodyIsAvailable(f, currentModule, inlineProtectedFunctions)) {

             // Don't inline opaque functions or foreign protected functions

           } else if (Attributes.Contains(f.Attributes, "no_inline")) {

             // User manually prevented inlining

-          } else if (CanSafelyInline(fexp, f)) {

-            // inline this body

-            var body = GetSubstitutedBody(fexp, f, false);

-            var typeSpecializedBody = GetSubstitutedBody(fexp, f, true);

-            var typeSpecializedResultType = Resolver.SubstType(f.ResultType, fexp.TypeArgumentSubstitutions);

-

+          } else {

             // Produce, for a "body" split into b0, b1, b2:

             //     checked F#canCall(args) ==> F(args) || b0

             //     checked F#canCall(args) ==> F(args) || b1

@@ -12999,49 +12994,62 @@ namespace Microsoft.Dafny {
             // F(args)

             fargs = etran.TrExpr(fexp);

 

-            // recurse on body

-            var ss = new List<SplitExprInfo>();

-            TrSplitExpr(typeSpecializedBody, ss, position, functionHeight, apply_induction, etran);

-            var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody);

-            foreach (var s in ss) {

-              if (s.IsChecked) {

-                var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type);

-                var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

-                var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok);

-                var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

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

+            if (!CanSafelyInline(fexp, f)) {

+              // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger

+              // TODO this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy

+              reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call cannot safely be inlined.");

+              // F#canCall(args) ==> F(args)

+              var p = Bpl.Expr.Binary(fargs.tok, BinaryOperator.Opcode.Imp, canCall, fargs);

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

+              // F#canCall(args) && F(args)

+              var fr = Bpl.Expr.And(canCall, fargs);

+              splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));

+

+            } else {

+              // inline this body

+              var typeSpecializedBody = GetSubstitutedBody(fexp, f);

+              var typeSpecializedResultType = Resolver.SubstType(f.ResultType, fexp.TypeArgumentSubstitutions);

+

+              // recurse on body

+              var ss = new List<SplitExprInfo>();

+              TrSplitExpr(typeSpecializedBody, ss, position, functionHeight, inlineProtectedFunctions, apply_induction, etran);

+              var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody);

+              foreach (var s in ss) {

+                if (s.IsChecked) {

+                  var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type);

+                  var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);

+                  var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok);

+                  var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);

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

+                }

               }

-            }

 

-            // allocatedness for arguments to the inlined call in body

-            if (typeSpecializedBody is FunctionCallExpr) {

-              FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody;

-              for (int i = 0; i < e.Args.Count; i++) {

-                Expression ee = e.Args[i];

-                Type t = e.Function.Formals[i].Type;

-                Expr tr_ee = etran.TrExpr(ee);

-                Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran);

-                if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); }

+              // allocatedness for arguments to the inlined call in body

+              if (typeSpecializedBody is FunctionCallExpr) {

+                FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody;

+                for (int i = 0; i < e.Args.Count; i++) {

+                  Expression ee = e.Args[i];

+                  Type t = e.Function.Formals[i].Type;

+                  Expr tr_ee = etran.TrExpr(ee);

+                  Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran);

+                  if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); }

+                }

               }

-            }

 

-            // body

-            var trBody = etran.TrExpr(typeSpecializedBody);

-            trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type);

-            // F#canCall(args) && F(args) && (b0 && b1 && b2)

-            var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody));

-            splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));

+              // body

+              var trBody = etran.TrExpr(typeSpecializedBody);

+              trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type);

+              // F#canCall(args) && F(args) && (b0 && b1 && b2)

+              var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody));

+              splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));

+            }

 

             return true;

-          } else {

-            // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger

-            // TODO this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy

-            reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call cannot safely be inlined.");

           }

         }

 

       } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier != null) {

-        return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, apply_induction, etran);

+        return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);

       } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr))

         /* NB: only for type arg less quantifiers for now: */

             && ((QuantifierExpr)expr).TypeArgs.Count == 0) {

@@ -13220,14 +13228,14 @@ namespace Microsoft.Dafny {
       }

     }

 

-    private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f, bool specializeTypeParameters) {

+    private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) {

       Contract.Requires(fexp != null);

       Contract.Requires(f != null);

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

       Contract.Assert(fexp.Args.Count == f.Formals.Count);

       for (int i = 0; i < f.Formals.Count; i++) {

         Formal p = f.Formals[i];

-        var formalType = specializeTypeParameters ? Resolver.SubstType(p.Type, fexp.TypeArgumentSubstitutions) : p.Type;

+        var formalType = Resolver.SubstType(p.Type, fexp.TypeArgumentSubstitutions);

         Expression arg = fexp.Args[i];

         arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), formalType);

         arg.Type = formalType;  // resolve here

@@ -13238,7 +13246,7 @@ namespace Microsoft.Dafny {
         var pp = (PrefixPredicate)f;

         body = PrefixSubstitution(pp, body);

       }

-      body = Substitute(body, fexp.Receiver, substMap, specializeTypeParameters ? fexp.TypeArgumentSubstitutions : null);

+      body = Substitute(body, fexp.Receiver, substMap, fexp.TypeArgumentSubstitutions);

       return body;

     }

 

diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect
index b3fb9cc0..b3d4ff34 100644
--- a/Test/dafny0/TriggerInPredicate.dfy.expect
+++ b/Test/dafny0/TriggerInPredicate.dfy.expect
@@ -2,5 +2,6 @@ TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)".
 TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z".

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

+TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 

 Dafny program verifier finished with 8 verified, 0 errors

diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect
index 808fe0f9..68b4ff73 100644
--- a/Test/dafny2/SnapshotableTrees.dfy.expect
+++ b/Test/dafny2/SnapshotableTrees.dfy.expect
@@ -1,8 +1,15 @@
 SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold.

 SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold.

+SnapshotableTrees.dfy(545,15): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold.

+SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold.

+SnapshotableTrees.dfy(548,18): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

 

-Dafny program verifier finished with 65 verified, 1 error

+Dafny program verifier finished with 65 verified, 2 errors

 Compiled assembly into SnapshotableTrees.exe

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
index 4c24893e..0b6f3e30 100644
--- a/Test/triggers/triggers-prevent-some-inlining.dfy.expect
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -3,5 +3,7 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call can
 triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.

 triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.

 triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.

+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.

+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.

 

 Dafny program verifier finished with 4 verified, 0 errors