diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index cf1388b50d9..08bcd71bf56 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/Source/DafnyCore/AST/AstVisitor.cs @@ -336,7 +336,7 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) { VisitUserProvidedType(local.SyntacticType, context); } - } else if (stmt is AssignStmt assignStmt) { + } else if (stmt is SingleAssignStmt assignStmt) { if (assignStmt.Rhs is TypeRhs typeRhs) { if (typeRhs.EType != null) { VisitUserProvidedType(typeRhs.EType, context); diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs index ea509b3c1a3..0e0fcdac78e 100644 --- a/Source/DafnyCore/AST/Expressions/StmtExpr.cs +++ b/Source/DafnyCore/AST/Expressions/StmtExpr.cs @@ -63,7 +63,7 @@ public Expression GetSConclusion() { return s.Result; } else if (S is HideRevealStmt) { return CreateBoolLiteral(tok, true); // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :) - } else if (S is UpdateStmt) { + } else if (S is AssignStatement) { return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :) } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index ef97d0be06f..43d093748d0 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -29,7 +29,10 @@ public partial class Printer { public void PrintStatement(Statement stmt, int indent) { Contract.Requires(stmt != null); - if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) { return; } + if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) { + return; + } + for (LList