From 9aaa0798bac4672064b75d311d23f7dc7e61bca7 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 19 Apr 2013 17:26:14 -0700
Subject: Fixed (completeness) bug in translation of automatic
 induction--previously, the induction-inserted 'forall' statement had caused
 the heap to be advanced).

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

(limited to 'Source/Dafny/Translator.cs')

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3d07a729..ff29df39 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2012,6 +2012,7 @@ namespace Microsoft.Dafny {
             }
             var recursiveCall = new CallStmt(m.tok, new List<Expression>(), recursiveCallReceiver, m.Name, recursiveCallArgs);
             recursiveCall.Method = m;  // resolve here
+            recursiveCall.IsGhost = m.IsGhost;  // resolve here
 
             Expression parRange = new LiteralExpr(m.tok, true);
             parRange.Type = Type.Bool;  // resolve here
-- 
cgit v1.2.3