Fixed bug that used != instead of == in one translation of fresh.

1 files changed, 2 insertions, 2 deletions

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index c5f85130..0b56372d 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -1673,9 +1673,9 @@ namespace Microsoft.Dafny {
             return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);

           } else {

             // generate:  x == null || !old($Heap)[x]

-            Bpl.Expr oNotNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null);

+            Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null);

             Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap));

-            return Bpl.Expr.Or(oNotNull, oIsFresh);

+            return Bpl.Expr.Or(oNull, oIsFresh);

           }

         

         } else if (expr is UnaryExpr) {