3 files changed, 23 insertions, 1 deletions
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
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d2ddc057..eb5b056a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1086,7 +1086,7 @@ Execution trace:
     (0,0): anon4_Else
     (0,0): anon3
 
-Dafny program verifier finished with 40 verified, 9 errors
+Dafny program verifier finished with 43 verified, 9 errors
 
 -------------------- TypeParameters.dfy --------------------
 TypeParameters.dfy(44,22): Error: assertion violation
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 4a9c0a31..e086ce73 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -292,3 +292,24 @@ method Empty_Parallel2()
   assert exists k :: EmptyPar_P(k);  // yes
   assert EmptyPar_P(8);  // error: the forall statement's ensures clause does not promise this
 }
+
+// ---------------------------------------------------------------------
+// The following is an example that once didn't verify (because the forall statement that
+// induction inserts had caused the $Heap to be advanced, despite the fact that Th is a
+// ghost method).
+
+datatype Nat = Zero | Succ(tail: Nat)
+
+predicate ThProperty(step: nat, t: Nat, r: nat)
+{
+  match t
+  case Zero => true
+  case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+}
+
+ghost method Th(step: nat, t: Nat, r: nat)
+  requires t.Succ? && ThProperty(step, t, r);
+  // the next line follows from the precondition and the definition of ThProperty
+  ensures exists ro:nat :: ThProperty(step-1, t.tail, ro);
+{
+}