Dafny implementation: removed always-true "allowGhostFeatures" parameter

1 files changed, 2 insertions, 3 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index ca19af7b..eb1d1cca 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2973,7 +2973,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignStmt) {

         AddComment(builder, stmt, "assignment statement");

         AssignStmt s = (AssignStmt)stmt;

-        TrAssignment(stmt.Tok, s.Lhs, s.Rhs, builder, locals, etran);

+        TrAssignment(stmt.Tok, s.Lhs.Resolved, s.Rhs, builder, locals, etran);

       } else if (stmt is VarDecl) {

         AddComment(builder, stmt, "var-declaration statement");

         VarDecl s = (VarDecl)stmt;

@@ -3903,14 +3903,13 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(tok != null);

       Contract.Requires(lhs != null);

-      // TODO:  Contract.Requires(!(lhs is ConcreteSyntaxExpression));

+      Contract.Requires(!(lhs is ConcreteSyntaxExpression));

       Contract.Requires(rhs != null);

       Contract.Requires(builder != null);

       Contract.Requires(cce.NonNullElements(locals));

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

 

-      lhs = lhs.Resolved;  // TODO: delete this line and instead bring in the commented-out precondition above

       TrStmt_CheckWellformed(lhs, builder, locals, etran, true);

 

       if (lhs is IdentifierExpr) {