Translate CanCallAssumption with the same fuel value as in the body of the function definition axiom (which prevents some matching loops)

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3eb06ebc..b0cdb3ae 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1854,7 +1854,7 @@ namespace Microsoft.Dafny {
           bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);

         }

         var etranBody = layer == null ? etran : etran.LimitedFunctions(f, new Bpl.IdentifierExpr(f.tok, layer));

-        meat = BplAnd(CanCallAssumption(bodyWithSubst, etran),

+        meat = BplAnd(CanCallAssumption(bodyWithSubst, etranBody),

           Bpl.Expr.Eq(funcAppl, etranBody.TrExpr(bodyWithSubst)));

       }

       QKeyValue kv = null;