From 07d9fdefae99507fea05a87b2887b50e83adb615 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Thu, 3 Jul 2014 15:01:26 -0700
Subject: Translate CanCallAssumption with the same fuel value as in the body
 of the function definition axiom (which prevents some matching loops)

---
 Source/Dafny/Translator.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;
-- 
cgit v1.2.3