Allow $Heap to occur in constraints (even though it isn't actually used)

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 53627053..367acba0 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -499,7 +499,9 @@ namespace Microsoft.Dafny {
             var ie = new IdentifierExpr(dd.tok, oVarDafny.Name);

             ie.Var = oVarDafny; ie.Type = ie.Var.Type;  // resolve ie here

             var constraint = etran.TrExpr(Substitute(dd.Constraint, dd.Var, ie));

-            rhs = BplAnd(rhs, constraint);

+            var heap = new Bpl.BoundVariable(dd.tok, new Bpl.TypedIdent(dd.tok, predef.HeapVarName, predef.HeapType));

+            var ex = new Bpl.ExistsExpr(dd.tok, new List<Variable> { heap }, constraint);

+            rhs = BplAnd(rhs, ex);

           }

           body = BplIff(is_o, rhs);

         }