Added proper parsing for StmtExpr's in all contexts.

Adjusted printer accordingly.
Fixed bug in Substituter for CalcStmt in StmtExpr's.
Always show terminating semi-colon in hover-text for default decreases clauses.

7 files changed, 511 insertions, 428 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index a0a8e699..5254d439 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -120,8 +120,8 @@ bool IsParenStar() {
   return la.kind == _openparen && x.kind == _star;

 }

 

-bool SemiFollowsCall(Expression e) {

-  return la.kind == _semi &&

+bool SemiFollowsCall(bool allowSemi, Expression e) {

+  return allowSemi && la.kind == _semi &&

     (e is FunctionCallExpr ||

      (e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));

 }

@@ -182,16 +182,16 @@ Dafny
      // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)

      Contract.Assert(defaultModule != null);

   .)

-  { "include" string							(. {

-													string parsedFile = t.filename;

-													string includedFile = t.val.Substring(1, t.val.Length - 2);

-													if (!Path.IsPathRooted(includedFile)) {

-													  string basePath = Path.GetDirectoryName(parsedFile);

-													  includedFile = Path.GetFullPath(Path.Combine(basePath, includedFile));

-													} 

-													defaultModule.Includes.Add(new Include(t, includedFile)); 

-													}

-												.) 

+  { "include" string                            (. {

+                                                    string parsedFile = t.filename;

+                                                    string includedFile = t.val.Substring(1, t.val.Length - 2);

+                                                    if (!Path.IsPathRooted(includedFile)) {

+                                                      string basePath = Path.GetDirectoryName(parsedFile);

+                                                      includedFile = Path.GetFullPath(Path.Combine(basePath, includedFile));

+                                                    } 

+                                                    defaultModule.Includes.Add(new Include(t, includedFile)); 

+                                                   }

+                                                .) 

   }

   { SubModuleDecl<defaultModule, out submodule> (. defaultModule.TopLevelDecls.Add(submodule); .)

   | ClassDecl<defaultModule, out c>             (. defaultModule.TopLevelDecls.Add(c); .)

@@ -609,20 +609,20 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   (. 

      if (!theVerifyThisFile) {

        body = null;

-	   

-		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-		Attributes.Argument/*!*/ anArg;

-		anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-		args.Add(anArg);

-		attrs = new Attributes("verify", args, attrs);

+       

+        List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

+        Attributes.Argument/*!*/ anArg;

+        anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

+        args.Add(anArg);

+        attrs = new Attributes("verify", args, attrs);

      }

 

-	 if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

-		SemErr(t, "only ghost methods can have the :axiom attribute");

+     if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

+        SemErr(t, "only ghost methods can have the :axiom attribute");

      }

 

      if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

-		SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

+        SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

      }

 

      if (isConstructor) {

@@ -655,8 +655,10 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
                ] SYNC ";"

   | [ "free"                                                 (. isFree = true; .)

     ]

-    ( "requires" Expression<out e> SYNC ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)

-    | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> } Expression<out e> SYNC ";"          (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)

+    ( "requires" Expression<out e, false> SYNC ";"           (. req.Add(new MaybeFreeExpression(e, isFree)); .)

+    | "ensures"

+      { IF(IsAttribute()) Attribute<ref ensAttrs> }

+      Expression<out e, false> SYNC ";"                      (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)

     )

   | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true> SYNC ";"

   )

@@ -682,14 +684,14 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
     ]

     [ "yield"                                                (. isYield = true; .)

     ]

-    ( "requires" Expression<out e> SYNC ";"                  (. if (isYield) {

+    ( "requires" Expression<out e, false> SYNC ";"           (. if (isYield) {

                                                                   yieldReq.Add(new MaybeFreeExpression(e, isFree));

                                                                 } else {

                                                                   req.Add(new MaybeFreeExpression(e, isFree));

                                                                 }

                                                              .)

     | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> }

-      Expression<out e> SYNC ";"                             (. if (isYield) {

+      Expression<out e, false> SYNC ";"                      (. if (isYield) {

                                                                   yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

                                                                 } else {

                                                                   ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));

@@ -868,18 +870,18 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   [ FunctionBody<out body, out bodyStart, out bodyEnd>

   ]

   (. if (!theVerifyThisFile) {  // We still need the func bodies, but don't bother verifying their correctness

-		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-		Attributes.Argument/*!*/ anArg;

-		anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-		args.Add(anArg);

-		attrs = new Attributes("verify", args, attrs);

-	 } 

+        List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

+        Attributes.Argument/*!*/ anArg;

+        anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

+        args.Add(anArg);

+        attrs = new Attributes("verify", args, attrs);

+     } 

 

      if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

-		SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

+        SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

      }

 

-	 if (isPredicate) {

+     if (isPredicate) {

         f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

                           reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);

      } else if (isCoPredicate) {

@@ -900,12 +902,12 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
      Expression/*!*/ e;  FrameExpression/*!*/ fe; .)

   (

     SYNC

-    "requires" Expression<out e> SYNC ";"      (. reqs.Add(e); .)

+    "requires" Expression<out e, false> SYNC ";"     (. reqs.Add(e); .)

   | "reads" [ PossiblyWildFrameExpression<out fe>              (. reads.Add(fe); .)

               { "," PossiblyWildFrameExpression<out fe>        (. reads.Add(fe); .)

               }

             ] SYNC ";"

-  | "ensures" Expression<out e> SYNC ";"      (. ens.Add(e); .)

+  | "ensures" Expression<out e, false> SYNC ";"      (. ens.Add(e); .)

   | "decreases"                               (. if (decreases == null) {

                                                    SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");

                                                    decreases = new List<Expression/*!*/>();

@@ -921,7 +923,7 @@ PossiblyWildExpression<out Expression/*!*/ e>
    * Use of this feature is sound only with respect to partial correctness.

    */

   ( "*"                        (. e = new WildcardExpr(t); .)

-  | Expression<out e>

+  | Expression<out e, false>

   )

   .

 PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>

@@ -943,7 +945,7 @@ FrameExpression<out FrameExpression/*!*/ fe>
      string fieldName = null;  IToken feTok = null;

      fe = null;

   .)

-  (( Expression<out e>          (. feTok = e.tok; .)

+  (( Expression<out e, false>   (. feTok = e.tok; .)

      [ "`" Ident<out id>        (. fieldName = id.val;  feTok = id; .)

      ]

                                 (. fe = new FrameExpression(feTok, e, fieldName); .)

@@ -956,7 +958,7 @@ FrameExpression<out FrameExpression/*!*/ fe>
 FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)

   "{"                         (. bodyStart = t; .)

-  ExpressionX<out e>

+  Expression<out e, true>

   "}"                         (. bodyEnd = t; .)

   .

 /*------------------------------------------------------------------------*/

@@ -1020,8 +1022,8 @@ SkeletonStmt<out Statement s>
      {"," Ident<out tok>               (. names.Add(tok); .)

      }

      ":=" 

-     Expression<out e>                 (. exprs.Add(e); .)

-     {"," Expression<out e>            (. exprs.Add(e); .)

+     Expression<out e, false>          (. exprs.Add(e); .)

+     {"," Expression<out e, false>     (. exprs.Add(e); .)

      }

                                        (. if (exprs.Count != names.Count) {

                                             SemErr(whereTok, exprs.Count < names.Count ? "not enough expressions" : "too many expressions");

@@ -1077,7 +1079,7 @@ UpdateStmt<out Statement/*!*/ s>
     | ":|"                         (. x = t; .)

       [ "assume"                   (. suchThatAssume = t; .)

       ]

-      Expression<out suchThat>

+      Expression<out suchThat, false>

     )

     ";"                            (. endTok = t; .)

   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)

@@ -1124,7 +1126,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
        }

     .)

   | "*"                                (. r = new HavocRhs(t); .)

-  | Expression<out e>                  (. r = new ExprRhs(e); .)

+  | Expression<out e, false>           (. r = new ExprRhs(e); .)

   )

   { Attribute<ref attrs> }             (. r.Attributes = attrs; .)

   .

@@ -1158,7 +1160,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
   | ":|"                           (. assignTok = t; .)

     [ "assume"                     (. suchThatAssume = t; .)

     ]

-    Expression<out suchThat>

+    Expression<out suchThat, false>

   ]

   ";"                              (. endTok = t; .)

   (. ConcreteUpdateStatement update;

@@ -1222,7 +1224,7 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives, out IToken endTok.>
   .)

   "{"

   { "case"                      (. x = t; .)

-    ExpressionX<out e>

+    Expression<out e, true>

     "=>"

     (. body = new List<Statement>(); .)

     { Stmt<body> }

@@ -1298,9 +1300,10 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
 Invariant<out MaybeFreeExpression/*!*/ invariant>

 = (. bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; .)

     SYNC

-    ["free"                                 (. isFree = true; .)

+    ["free"                            (. isFree = true; .)

     ]

-    "invariant" { IF(IsAttribute()) Attribute<ref attrs> } Expression<out e>           (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)

+    "invariant" { IF(IsAttribute()) Attribute<ref attrs> }

+    Expression<out e, false>           (. invariant = new MaybeFreeExpression(e, isFree, attrs); .)

   .

 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

@@ -1322,7 +1325,7 @@ Guard<out Expression e>   /* null represents demonic-choice */
 = (. Expression/*!*/ ee;  e = null; .)

   ( "*"                             (. e = null; .)

   | IF(IsParenStar())  "(" "*" ")"  (. e = null; .)

-  | ExpressionX<out ee>             (. e = ee; .)

+  | Expression<out ee, true>        (. e = ee; .)

   )

   .

 MatchStmt<out Statement/*!*/ s>

@@ -1330,7 +1333,7 @@ MatchStmt<out Statement/*!*/ s>
      Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

      List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); .)

   "match"                     (. x = t; .)

-  ExpressionX<out e>

+  Expression<out e, true>

   "{"

   { CaseStatement<out c>     (. cases.Add(c); .)

   }

@@ -1362,7 +1365,7 @@ AssertStmt<out Statement/*!*/ s>
   .)

   "assert"                                     (. x = t; .)

   { IF(IsAttribute()) Attribute<ref attrs> }

-  ( Expression<out e>

+  ( Expression<out e, false>

   | "..."

   )

   ";"

@@ -1379,7 +1382,7 @@ AssumeStmt<out Statement/*!*/ s>
   .)

   "assume"                                     (. x = t; .)

   { IF(IsAttribute()) Attribute<ref attrs> }

-  ( Expression<out e>

+  ( Expression<out e, false>

   | "..."

   )

   ";"

@@ -1395,8 +1398,8 @@ PrintStmt<out Statement/*!*/ s>
      List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

   .)

   "print"                                      (. x = t; .)

-  AttributeArg<out arg>                        (. args.Add(arg); .)

-  { "," AttributeArg<out arg>                  (. args.Add(arg); .)

+  AttributeArg<out arg, false>                 (. args.Add(arg); .)

+  { "," AttributeArg<out arg, false>           (. args.Add(arg); .)

   }

   ";"                                          (. s = new PrintStmt(x, t, args); .)

   .

@@ -1435,7 +1438,7 @@ ForallStmt<out Statement/*!*/ s>
   {                                         (. isFree = false; .)

     [ "free"                                (. isFree = true; .)

     ]

-    "ensures" Expression<out e> ";"         (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

+    "ensures" Expression<out e, false> ";"  (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

   }

   BlockStmt<out block, out bodyStart, out bodyEnd>

   (. s = new ForallStmt(x, block.EndTok, bvars, attrs, range, ens, block); .)

@@ -1464,7 +1467,7 @@ CalcStmt<out Statement/*!*/ s>
                                                           .)

   ]

   "{"

-  { Expression<out e>                                     (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .)

+  { Expression<out e, false>                              (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .)

     ";"

     [ CalcOp<out opTok, out op>                           (. maybeOp = resOp.ResultOp(op);

                                                              if (maybeOp == null) {

@@ -1498,7 +1501,7 @@ CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
      x = null;

   .)

   ( "=="           (. x = t;  binOp = BinaryExpr.Opcode.Eq; .)

-    [ "#" "[" ExpressionX<out k> "]" ]

+    [ "#" "[" Expression<out k, true> "]" ]

   | "<"            (. x = t;  binOp = BinaryExpr.Opcode.Lt; .)

   | ">"            (. x = t;  binOp = BinaryExpr.Opcode.Gt; .)

   | "<="           (. x = t;  binOp = BinaryExpr.Opcode.Le; .)

@@ -1535,73 +1538,74 @@ Hint<out BlockStmt s>
   .)

   .

 /*------------------------------------------------------------------------*/

-ExpressionX<out Expression/*!*/ e>

+/* The "allowSemi" argument says whether or not the top-level expression

+ * to be parsed is allowed to have the form S;E where S is a call to a lemma.

+ * "allowSemi" should be passed in as "false" whenever the expression to

+ * be parsed sits in a context that itself is terminated by a semi-colon.

+ */

+Expression<out Expression e, bool allowSemi>

 = (. Expression e0; IToken endTok; .)

-  Expression<out e>

-  [ IF(SemiFollowsCall(e))

+  EquivExpression<out e, allowSemi>

+  [ IF(SemiFollowsCall(allowSemi, e))

     ";"                       (. endTok = t; .)

-    ExpressionX<out e0>

+    Expression<out e0, allowSemi>

     (. e = new StmtExpr(e.tok,

              new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),

              e0);

     .)

   ]

   .

-Expression<out Expression/*!*/ e>

-=

-  EquivExpression<out e>

-  .

 /*------------------------------------------------------------------------*/

-EquivExpression<out Expression/*!*/ e0>

+EquivExpression<out Expression e0, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

-  ImpliesExpliesExpression<out e0>

-  { EquivOp                                    (. x = t; .)

-    ImpliesExpliesExpression<out e1>           (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)

+  ImpliesExpliesExpression<out e0, allowSemi>

+  { EquivOp                                      (. x = t; .)

+    ImpliesExpliesExpression<out e1, allowSemi>  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)

   }

   .

 EquivOp = "<==>" | '\u21d4'.

 /*------------------------------------------------------------------------*/

-ImpliesExpliesExpression<out Expression/*!*/ e0>

+ImpliesExpliesExpression<out Expression e0, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

-  LogicalExpression<out e0>

+  LogicalExpression<out e0, allowSemi>

   [ ImpliesOp                                  (. x = t; .)

-    ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

+    ImpliesExpression<out e1, allowSemi>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

   | ExpliesOp                                  (. x = t; .)

-    LogicalExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

+    LogicalExpression<out e1, allowSemi>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

     { ExpliesOp                                (. x = t; .)

-      LogicalExpression<out e1>                (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

+      LogicalExpression<out e1, allowSemi>     (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

     }

   ]

   .

-ImpliesExpression<out Expression/*!*/ e0>

+ImpliesExpression<out Expression e0, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

-  LogicalExpression<out e0>

+  LogicalExpression<out e0, allowSemi>

   [ ImpliesOp                                  (. x = t; .)

-    ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

+    ImpliesExpression<out e1, allowSemi>       (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

   ]

   .

 ImpliesOp = "==>" | '\u21d2'.

 ExpliesOp = "<==" | '\u21d0'.

 /*------------------------------------------------------------------------*/

-LogicalExpression<out Expression/*!*/ e0>

+LogicalExpression<out Expression e0, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; .)

-  RelationalExpression<out e0>

+  RelationalExpression<out e0, allowSemi>

   [ AndOp                                      (. x = t; .)

-    RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)

+    RelationalExpression<out e1, allowSemi>    (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)

     { AndOp                                    (. x = t; .)

-      RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)

+      RelationalExpression<out e1, allowSemi>  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); .)

     }

   | OrOp                                       (. x = t; .)

-    RelationalExpression<out e1>               (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)

+    RelationalExpression<out e1, allowSemi>    (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)

     { OrOp                                     (. x = t; .)

-      RelationalExpression<out e1>             (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)

+      RelationalExpression<out e1, allowSemi>  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); .)

     }

   ]

   .

 AndOp = "&&" | '\u2227'.

 OrOp = "||" | '\u2228'.

 /*------------------------------------------------------------------------*/

-RelationalExpression<out Expression/*!*/ e>

+RelationalExpression<out Expression e, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

      IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;

      List<Expression> chain = null;

@@ -1615,9 +1619,9 @@ RelationalExpression<out Expression/*!*/ e>
                     // 4 ("disjoint")    indicates chain of disjoint set operators

      bool hasSeenNeq = false;

   .)

-  Term<out e0>                     (. e = e0; .)

+  Term<out e0, allowSemi>          (. e = e0; .)

   [ RelOp<out x, out op, out k>    (. firstOpTok = x; .)

-    Term<out e1>                   (. if (k == null) {

+    Term<out e1, allowSemi>        (. if (k == null) {

                                         e = new BinaryExpr(x, op, e0, e1);

                                         if (op == BinaryExpr.Opcode.Disjoint)

                                           acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

@@ -1676,7 +1680,7 @@ RelationalExpression<out Expression/*!*/ e>
                                           kind = 3;  break;

                                       }

                                    .)

-      Term<out e1>                 (. ops.Add(op); prefixLimits.Add(k); chain.Add(e1);

+      Term<out e1, allowSemi>      (. ops.Add(op); prefixLimits.Add(k); chain.Add(e1);

                                       if (k != null) {

                                         Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);

                                         e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);

@@ -1701,13 +1705,13 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k>
      k = null;

   .)

   ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)

-    [ "#" "[" ExpressionX<out k> "]" ]

+    [ "#" "[" Expression<out k, true> "]" ]

   | "<"            (. x = t;  op = BinaryExpr.Opcode.Lt; .)

   | ">"            (. x = t;  op = BinaryExpr.Opcode.Gt; .)

   | "<="           (. x = t;  op = BinaryExpr.Opcode.Le; .)

   | ">="           (. x = t;  op = BinaryExpr.Opcode.Ge; .)

   | "!="           (. x = t;  op = BinaryExpr.Opcode.Neq; .)

-    [ "#" "[" ExpressionX<out k> "]" ]

+    [ "#" "[" Expression<out k, true> "]" ]

   | "in"           (. x = t;  op = BinaryExpr.Opcode.In; .)

   | notIn          (. x = t;  op = BinaryExpr.Opcode.NotIn; .)

   | /* The next operator is "!!", but we have to scan it as two "!", since the scanner is gready 

@@ -1729,28 +1733,28 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k>
   )

   .

 /*------------------------------------------------------------------------*/

-Term<out Expression/*!*/ e0>

+Term<out Expression e0, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)

-  Factor<out e0>

+  Factor<out e0, allowSemi>

   { AddOp<out x, out op>

-    Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)

+    Factor<out e1, allowSemi>            (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

-AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

-=          (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)

+AddOp<out IToken x, out BinaryExpr.Opcode op>

+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; .)

   ( "+"            (. x = t;  op = BinaryExpr.Opcode.Add; .)

   | "-"            (. x = t;  op = BinaryExpr.Opcode.Sub; .)

   )

   .

 /*------------------------------------------------------------------------*/

-Factor<out Expression/*!*/ e0>

+Factor<out Expression e0, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; .)

-  UnaryExpression<out e0>

+  UnaryExpression<out e0, allowSemi>

   { MulOp<out x, out op>

-    UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)

+    UnaryExpression<out e1, allowSemi>              (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

-MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

+MulOp<out IToken x, out BinaryExpr.Opcode op>

 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; .)

   ( "*"            (. x = t;  op = BinaryExpr.Opcode.Mul; .)

   | "/"            (. x = t;  op = BinaryExpr.Opcode.Div; .)

@@ -1758,13 +1762,13 @@ MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   )

   .

 /*------------------------------------------------------------------------*/

-UnaryExpression<out Expression/*!*/ e>

+UnaryExpression<out Expression e, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; .)

   ( "-"                                        (. x = t; .)

-    UnaryExpression<out e>                     (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)

+    UnaryExpression<out e, allowSemi>          (. e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); .)

   | NegOp                                      (. x = t; .)

-    UnaryExpression<out e>                     (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)

-  | EndlessExpression<out e>     /* these have no further suffix */

+    UnaryExpression<out e, allowSemi>          (. e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); .)

+  | EndlessExpression<out e, allowSemi>   /* these have no further suffix */

   | DottedIdentifiersAndFunction<out e>

     { Suffix<ref e> }

   | DisplayExpr<out e>

@@ -1774,7 +1778,7 @@ UnaryExpression<out Expression/*!*/ e>
   | "map"                                      (. x = t; .)

     ( MapDisplayExpr<x, out e>

       { Suffix<ref e> }

-    | MapComprehensionExpr<x, out e>

+    | MapComprehensionExpr<x, out e, allowSemi>

     | (. SemErr("map must be followed by literal in brackets or comprehension."); .)

     )

   | ConstAtomExpression<out e>

@@ -1796,7 +1800,7 @@ NegOp = "!" | '\u00ac'.
  * an open paren (but could very well have a suffix that starts with a period or a square bracket).

  * (The "Also..." part may change if expressions in Dafny could yield functions.)

  */

-ConstAtomExpression<out Expression/*!*/ e>

+ConstAtomExpression<out Expression e>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

      IToken/*!*/ x;  BigInteger n;

      e = dummyExpr;

@@ -1807,14 +1811,14 @@ ConstAtomExpression<out Expression/*!*/ e>
   | Nat<out n>                                 (. e = new LiteralExpr(t, n); .)

   | "this"                                     (. e = new ThisExpr(t); .)

   | "fresh"                                    (. x = t; .)

-    "(" Expression<out e> ")"                  (. e = new FreshExpr(x, e); .)

+    "(" Expression<out e, true> ")"            (. e = new FreshExpr(x, e); .)

   | "old"                                      (. x = t; .)

-    "(" Expression<out e> ")"                  (. e = new OldExpr(x, e); .)

+    "(" Expression<out e, true> ")"            (. e = new OldExpr(x, e); .)

   | "|"                                        (. x = t; .)

-      Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

+      Expression<out e, true>                  (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

   | "("                                        (. x = t; .)

-      Expression<out e>                        (. e = new ParensExpression(x, e); .)

+      Expression<out e, true>                  (. e = new ParensExpression(x, e); .)

     ")"

   )

   .

@@ -1841,7 +1845,7 @@ MultiSetExpr<out Expression e>
       [ Expressions<elements> ]                (. e = new MultiSetDisplayExpr(x, elements);.)

     "}"

   | "("                                        (. x = t;  elements = new List<Expression/*!*/>(); .)

-      ExpressionX<out e>                       (. e = new MultiSetFormingExpr(x, e); .)

+      Expression<out e, true>                  (. e = new MultiSetFormingExpr(x, e); .)

     ")"

   | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)

   )

@@ -1858,41 +1862,41 @@ MapDisplayExpr<IToken/*!*/ mapToken, out Expression e>
 MapLiteralExpressions<.out List<ExpressionPair> elements.>

 = (. Expression/*!*/ d, r;

      elements = new List<ExpressionPair/*!*/>(); .)

-  ExpressionX<out d> ":=" ExpressionX<out r>       (. elements.Add(new ExpressionPair(d,r)); .)

-  { "," ExpressionX<out d> ":=" ExpressionX<out r> (. elements.Add(new ExpressionPair(d,r)); .)

+  Expression<out d, true> ":=" Expression<out r, true>       (. elements.Add(new ExpressionPair(d,r)); .)

+  { "," Expression<out d, true> ":=" Expression<out r, true> (. elements.Add(new ExpressionPair(d,r)); .)

   }

   .

-MapComprehensionExpr<IToken/*!*/ mapToken, out Expression e>

+MapComprehensionExpr<IToken mapToken, out Expression e, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-     BoundVar/*!*/ bv;

-     List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

+     BoundVar bv;

+     List<BoundVar> bvars = new List<BoundVar>();

      Expression range = null;

      Expression body;

   .)

   IdentTypeOptional<out bv>                    (. bvars.Add(bv); .)

-  [ "|" Expression<out range> ]

+  [ "|" Expression<out range, true> ]

   QSep

-  Expression<out body>

+  Expression<out body, allowSemi>

   (. e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);

   .)

   .

-EndlessExpression<out Expression e>

+EndlessExpression<out Expression e, bool allowSemi>

 = (. IToken/*!*/ x;

      Expression e0, e1;

      Statement s;

      e = dummyExpr;

   .)

   ( "if"                            (. x = t; .)

-    Expression<out e>

-    "then" Expression<out e0>

-    "else" Expression<out e1>       (. e = new ITEExpr(x, e, e0, e1); .)

-  | MatchExpression<out e>

-  | QuantifierGuts<out e>

-  | ComprehensionExpr<out e>

+    Expression<out e, true>

+    "then" Expression<out e0, true>

+    "else" Expression<out e1, allowSemi>       (. e = new ITEExpr(x, e, e0, e1); .)

+  | MatchExpression<out e, allowSemi>

+  | QuantifierGuts<out e, allowSemi>

+  | ComprehensionExpr<out e, allowSemi>

   | StmtInExpr<out s>

-    Expression<out e>               (. e = new StmtExpr(s.Tok, s, e); .)

-  | LetExpr<out e>

-  | NamedExpr<out e>

+    Expression<out e, allowSemi>               (. e = new StmtExpr(s.Tok, s, e); .)

+  | LetExpr<out e, allowSemi>

+  | NamedExpr<out e, allowSemi>

   )

   .

 

@@ -1904,7 +1908,7 @@ StmtInExpr<out Statement s>
   )

   .

 

-LetExpr<out Expression e>

+LetExpr<out Expression e, bool allowSemi>

 = (. IToken/*!*/ x;

      e = dummyExpr;

      BoundVar d;

@@ -1920,14 +1924,14 @@ LetExpr<out Expression e>
     ( ":="

     | ":|"                          (. exact = false; .)

     )

-    Expression<out e>               (. letRHSs.Add(e); .)

-    { "," Expression<out e>         (. letRHSs.Add(e); .)

+    Expression<out e, false>        (. letRHSs.Add(e); .)

+    { "," Expression<out e, false>  (. letRHSs.Add(e); .)

     }

     ";"

-    Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e, exact); .)

+    Expression<out e, allowSemi>    (. e = new LetExpr(x, letVars, letRHSs, e, exact); .)

   .

 

-NamedExpr<out Expression e>

+NamedExpr<out Expression e, bool allowSemi>

 = (. IToken/*!*/ x, d;

      e = dummyExpr;

      Expression expr;

@@ -1935,24 +1939,24 @@ NamedExpr<out Expression e>
     "label"                          (. x = t; .)

     NoUSIdent<out d>

     ":"

-    Expression<out e>               (. expr = e;

-                                       e = new NamedExpr(x, d.val, expr); .)

+    Expression<out e, allowSemi>     (. expr = e;

+                                        e = new NamedExpr(x, d.val, expr); .)

   .

 

-MatchExpression<out Expression/*!*/ e>

+MatchExpression<out Expression e, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

      List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

   .)

   "match"                     (. x = t; .)

-  Expression<out e>

+  Expression<out e, allowSemi>

   /* Note: The following gives rise to a '"case" is start & successor of deletable structure' error,

      but it's okay, because we want this closer match expression to bind as much as possible--use

      parens around it to limit its scope. */

-  { CaseExpression<out c>     (. cases.Add(c); .)

+  { CaseExpression<out c, allowSemi>     (. cases.Add(c); .)

   }

   (. e = new MatchExpr(x, e, cases); .)

   .

-CaseExpression<out MatchCaseExpr/*!*/ c>

+CaseExpression<out MatchCaseExpr c, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;

      List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

      BoundVar/*!*/ bv;

@@ -1966,7 +1970,7 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
     }

   ")" ]

   "=>"

-  Expression<out body>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)

+  Expression<out body, allowSemi>    (. c = new MatchCaseExpr(x, id.val, arguments, body); .)

   .

 /*------------------------------------------------------------------------*/

 DottedIdentifiersAndFunction<out Expression e>

@@ -1980,7 +1984,7 @@ DottedIdentifiersAndFunction<out Expression e>
   }

   [                                    (. args = new List<Expression>(); .)

     [ "#"                              (. id.val = id.val + "#";  Expression k; .)

-      "[" ExpressionX<out k> "]"       (. args.Add(k); .)

+      "[" Expression<out k, true> "]"  (. args.Add(k); .)

     ]

     "("                                (. openParen = t; .)

       [ Expressions<args> ]

@@ -1988,7 +1992,7 @@ DottedIdentifiersAndFunction<out Expression e>
   ]

   (. e = new IdentifierSequence(idents, openParen, args); .)

   .

-Suffix<ref Expression/*!*/ e>

+Suffix<ref Expression e>

 = (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x;  List<Expression/*!*/>/*!*/ args;

      Expression e0 = null;  Expression e1 = null;  Expression/*!*/ ee;  bool anyDots = false;

      List<Expression> multipleIndices = null;

@@ -1998,20 +2002,20 @@ Suffix<ref Expression/*!*/ e>
     IdentOrDigits<out id>

     [                                          (. args = new List<Expression/*!*/>();  func = true; .)

       [ "#"                                    (. id.val = id.val + "#";  Expression k; .)

-        "[" ExpressionX<out k> "]"             (. args.Add(k); .)

+        "[" Expression<out k, true> "]"        (. args.Add(k); .)

       ]

       "("                                      (. IToken openParen = t; .)

         [ Expressions<args> ]

       ")"                                      (. e = new FunctionCallExpr(id, id.val, e, openParen, args); .)

     ]                                          (. if (!func) { e = new ExprDotName(id, e, id.val); } .)

   | "["                                        (. x = t; .)

-      ( ExpressionX<out ee>                    (. e0 = ee; .)

+      ( Expression<out ee, true>               (. e0 = ee; .)

         ( ".."                                 (. anyDots = true; .)

-          [ ExpressionX<out ee>                (. e1 = ee; .)

+          [ Expression<out ee, true>           (. e1 = ee; .)

           ]

         | ":="

-          ExpressionX<out ee>                  (. e1 = ee; .)

-        | { "," ExpressionX<out ee>            (. if (multipleIndices == null) {

+          Expression<out ee, true>             (. e1 = ee; .)

+        | { "," Expression<out ee, true>       (. if (multipleIndices == null) {

                                                     multipleIndices = new List<Expression>();

                                                     multipleIndices.Add(e0);

                                                   }

@@ -2020,7 +2024,7 @@ Suffix<ref Expression/*!*/ e>
           }

         )

       | ".."                                   (. anyDots = true; .)

-        [ ExpressionX<out ee>                  (. e1 = ee; .)

+        [ Expression<out ee, true>             (. e1 = ee; .)

         ]

       )

       (. if (multipleIndices != null) {

@@ -2049,7 +2053,7 @@ Suffix<ref Expression/*!*/ e>
   )

   .

 /*------------------------------------------------------------------------*/

-QuantifierGuts<out Expression/*!*/ q>

+QuantifierGuts<out Expression q, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;

      bool univ = false;

      List<BoundVar/*!*/> bvars;

@@ -2062,7 +2066,7 @@ QuantifierGuts<out Expression/*!*/ q>
   )

   QuantifierDomain<out bvars, out attrs, out range>

   QSep

-  Expression<out body>

+  Expression<out body, allowSemi>

   (. if (univ) {

        q = new ForallExpr(x, bvars, range, body, attrs);

      } else {

@@ -2075,9 +2079,9 @@ Forall = "forall" | '\u2200'.
 Exists = "exists" | '\u2203'.

 QSep = "::" | '\u2022'.

 

-QuantifierDomain<.out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range.>

+QuantifierDomain<.out List<BoundVar> bvars, out Attributes attrs, out Expression range.>

 = (.

-     bvars = new List<BoundVar/*!*/>();

+     bvars = new List<BoundVar>();

      BoundVar/*!*/ bv;

      attrs = null;

      range = null;

@@ -2088,16 +2092,16 @@ QuantifierDomain<.out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expre
   }

   { IF(IsAttribute()) Attribute<ref attrs> }

   [ "|"

-    Expression<out range>

+    Expression<out range, true>

   ]

   .

 

-ComprehensionExpr<out Expression/*!*/ q>

+ComprehensionExpr<out Expression q, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);

-     IToken/*!*/ x = Token.NoToken;

-     BoundVar/*!*/ bv;

-     List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

-     Expression/*!*/ range;

+     IToken x = Token.NoToken;

+     BoundVar bv;

+     List<BoundVar/*!*/> bvars = new List<BoundVar>();

+     Expression range;

      Expression body = null;

   .)

   "set"                                        (. x = t; .)

@@ -2105,10 +2109,10 @@ ComprehensionExpr<out Expression/*!*/ q>
   { ","

     IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)

   }

-  "|" Expression<out range>

+  "|" Expression<out range, allowSemi>

   [

     QSep

-    Expression<out body>

+    Expression<out body, allowSemi>

   ]

   (. if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

      q = new SetComprehension(x, bvars, range, body);

@@ -2116,8 +2120,8 @@ ComprehensionExpr<out Expression/*!*/ q>
   .

 Expressions<.List<Expression/*!*/>/*!*/ args.>

 = (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)

-  ExpressionX<out e>                           (. args.Add(e); .)

-  { "," ExpressionX<out e>                     (. args.Add(e); .)

+  Expression<out e, true>                      (. args.Add(e); .)

+  { "," Expression<out e, true>                (. args.Add(e); .)

   }

   .

 /*------------------------------------------------------------------------*/

@@ -2132,15 +2136,15 @@ AttributeBody<ref Attributes attrs>
      Attributes.Argument/*!*/ aArg;

   .)

   ":" ident                            (. aName = t.val; .)

-  [ AttributeArg<out aArg>             (. aArgs.Add(aArg); .)

-    { "," AttributeArg<out aArg>       (. aArgs.Add(aArg); .)

+  [ AttributeArg<out aArg, true>       (. aArgs.Add(aArg); .)

+    { "," AttributeArg<out aArg, true> (. aArgs.Add(aArg); .)

     }

   ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)

   .

-AttributeArg<out Attributes.Argument/*!*/ arg>

+AttributeArg<out Attributes.Argument arg, bool allowSemi>

 = (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e;  arg = dummyAttrArg; .)

   ( string                             (. arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); .)

-  | ExpressionX<out e>                 (. arg = new Attributes.Argument(t, e); .)

+  | Expression<out e, allowSemi>       (. arg = new Attributes.Argument(t, e); .)

   )

   .

 /*------------------------------------------------------------------------*/

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index b1531a65..e96f8bd8 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -145,8 +145,8 @@ bool IsParenStar() {
   return la.kind == _openparen && x.kind == _star;

 }

 

-bool SemiFollowsCall(Expression e) {

-  return la.kind == _semi &&

+bool SemiFollowsCall(bool allowSemi, Expression e) {

+  return allowSemi && la.kind == _semi &&

     (e is FunctionCallExpr ||

      (e is IdentifierSequence && ((IdentifierSequence)e).OpenParen != null));

 }

@@ -237,8 +237,8 @@ bool SemiFollowsCall(Expression e) {
 			string parsedFile = t.filename;

 			string includedFile = t.val.Substring(1, t.val.Length - 2);

 			if (!Path.IsPathRooted(includedFile)) {

-			string basePath = Path.GetDirectoryName(parsedFile);

-			includedFile = Path.GetFullPath(Path.Combine(basePath, includedFile));

+			  string basePath = Path.GetDirectoryName(parsedFile);

+			  includedFile = Path.GetFullPath(Path.Combine(basePath, includedFile));

 			} 

 			defaultModule.Includes.Add(new Include(t, includedFile)); 

 			}

@@ -786,15 +786,15 @@ bool SemiFollowsCall(Expression e) {
 			FunctionBody(out body, out bodyStart, out bodyEnd);

 		}

 		if (!theVerifyThisFile) {  // We still need the func bodies, but don't bother verifying their correctness

-		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-		Attributes.Argument/*!*/ anArg;

-		anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-		args.Add(anArg);

-		attrs = new Attributes("verify", args, attrs);

+		  List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

+		  Attributes.Argument/*!*/ anArg;

+		  anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

+		  args.Add(anArg);

+		  attrs = new Attributes("verify", args, attrs);

 		} 

 		

 		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

-		SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

+		  SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");

 		}

 		

 		if (isPredicate) {

@@ -910,20 +910,20 @@ bool SemiFollowsCall(Expression e) {
 		}

 		if (!theVerifyThisFile) {

 		 body = null;

-		

-		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

-		Attributes.Argument/*!*/ anArg;

-		anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

-		args.Add(anArg);

-		attrs = new Attributes("verify", args, attrs);

+		 

+		  List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

+		  Attributes.Argument/*!*/ anArg;

+		  anArg = new Attributes.Argument(id, new LiteralExpr(t, false));

+		  args.Add(anArg);

+		  attrs = new Attributes("verify", args, attrs);

 		}

 		

 		if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

-		SemErr(t, "only ghost methods can have the :axiom attribute");

+		  SemErr(t, "only ghost methods can have the :axiom attribute");

 		}

 		

 		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

-		SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

+		  SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

 		}

 		

 		if (isConstructor) {

@@ -1224,7 +1224,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 			}

 			if (la.kind == 47) {

 				Get();

-				Expression(out e);

+				Expression(out e, false);

 				while (!(la.kind == 0 || la.kind == 7)) {SynErr(150); Get();}

 				Expect(7);

 				if (isYield) {

@@ -1238,7 +1238,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

-				Expression(out e);

+				Expression(out e, false);

 				while (!(la.kind == 0 || la.kind == 7)) {SynErr(151); Get();}

 				Expect(7);

 				if (isYield) {

@@ -1302,7 +1302,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			if (la.kind == 47) {

 				Get();

-				Expression(out e);

+				Expression(out e, false);

 				while (!(la.kind == 0 || la.kind == 7)) {SynErr(157); Get();}

 				Expect(7);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

@@ -1311,7 +1311,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

 				}

-				Expression(out e);

+				Expression(out e, false);

 				while (!(la.kind == 0 || la.kind == 7)) {SynErr(158); Get();}

 				Expect(7);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

@@ -1335,7 +1335,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		fe = null;

 		

 		if (StartOf(16)) {

-			Expression(out e);

+			Expression(out e, false);

 			feTok = e.tok; 

 			if (la.kind == 63) {

 				Get();

@@ -1351,8 +1351,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(162);

 	}

 

-	void Expression(out Expression/*!*/ e) {

-		EquivExpression(out e);

+	void Expression(out Expression e, bool allowSemi) {

+		Expression e0; IToken endTok; 

+		EquivExpression(out e, allowSemi);

+		if (SemiFollowsCall(allowSemi, e)) {

+			Expect(7);

+			endTok = t; 

+			Expression(out e0, allowSemi);

+			e = new StmtExpr(e.tok,

+			     new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),

+			     e0);

+			

+		}

 	}

 

 	void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {

@@ -1435,7 +1445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 47) {

 			while (!(la.kind == 0 || la.kind == 47)) {SynErr(164); Get();}

 			Get();

-			Expression(out e);

+			Expression(out e, false);

 			while (!(la.kind == 0 || la.kind == 7)) {SynErr(165); Get();}

 			Expect(7);

 			reqs.Add(e); 

@@ -1454,7 +1464,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(7);

 		} else if (la.kind == 48) {

 			Get();

-			Expression(out e);

+			Expression(out e, false);

 			while (!(la.kind == 0 || la.kind == 7)) {SynErr(167); Get();}

 			Expect(7);

 			ens.Add(e); 

@@ -1475,7 +1485,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 

 		Expect(8);

 		bodyStart = t; 

-		ExpressionX(out e);

+		Expression(out e, true);

 		Expect(9);

 		bodyEnd = t; 

 	}

@@ -1497,24 +1507,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			e = new WildcardExpr(t); 

 		} else if (StartOf(16)) {

-			Expression(out e);

+			Expression(out e, false);

 		} else SynErr(171);

 	}

 

-	void ExpressionX(out Expression/*!*/ e) {

-		Expression e0; IToken endTok; 

-		Expression(out e);

-		if (SemiFollowsCall(e)) {

-			Expect(7);

-			endTok = t; 

-			ExpressionX(out e0);

-			e = new StmtExpr(e.tok,

-			     new UpdateStmt(e.tok, endTok, new List<Expression>(), new List<AssignmentRhs>() { new ExprRhs(e, null) }),

-			     e0);

-			

-		}

-	}

-

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

 		Statement/*!*/ s;

 		

@@ -1624,7 +1620,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Attribute(ref attrs);

 		}

 		if (StartOf(16)) {

-			Expression(out e);

+			Expression(out e, false);

 		} else if (la.kind == 37) {

 			Get();

 		} else SynErr(176);

@@ -1647,7 +1643,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Attribute(ref attrs);

 		}

 		if (StartOf(16)) {

-			Expression(out e);

+			Expression(out e, false);

 		} else if (la.kind == 37) {

 			Get();

 		} else SynErr(177);

@@ -1666,11 +1662,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(82);

 		x = t; 

-		AttributeArg(out arg);

+		AttributeArg(out arg, false);

 		args.Add(arg); 

 		while (la.kind == 30) {

 			Get();

-			AttributeArg(out arg);

+			AttributeArg(out arg, false);

 			args.Add(arg); 

 		}

 		Expect(7);

@@ -1719,7 +1715,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					suchThatAssume = t; 

 				}

-				Expression(out suchThat);

+				Expression(out suchThat, false);

 			} else SynErr(178);

 			Expect(7);

 			endTok = t; 

@@ -1790,7 +1786,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					suchThatAssume = t; 

 				}

-				Expression(out suchThat);

+				Expression(out suchThat, false);

 			}

 		}

 		Expect(7);

@@ -1918,7 +1914,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 

 		Expect(80);

 		x = t; 

-		ExpressionX(out e);

+		Expression(out e, true);

 		Expect(8);

 		while (la.kind == 76) {

 			CaseStatement(out c);

@@ -1976,7 +1972,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				isFree = true; 

 			}

 			Expect(48);

-			Expression(out e);

+			Expression(out e, false);

 			Expect(7);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

 		}

@@ -2011,7 +2007,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(8);

 		while (StartOf(16)) {

-			Expression(out e);

+			Expression(out e, false);

 			lines.Add(e); stepOp = calcOp; danglingOperator = null; 

 			Expect(7);

 			if (StartOf(21)) {

@@ -2093,11 +2089,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				names.Add(tok); 

 			}

 			Expect(67);

-			Expression(out e);

+			Expression(out e, false);

 			exprs.Add(e); 

 			while (la.kind == 30) {

 				Get();

-				Expression(out e);

+				Expression(out e, false);

 				exprs.Add(e); 

 			}

 			if (exprs.Count != names.Count) {

@@ -2156,7 +2152,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			r = new HavocRhs(t); 

 		} else if (StartOf(16)) {

-			Expression(out e);

+			Expression(out e, false);

 			r = new ExprRhs(e); 

 		} else SynErr(187);

 		while (la.kind == 8) {

@@ -2184,11 +2180,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

 		Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; 

-		ExpressionX(out e);

+		Expression(out e, true);

 		args.Add(e); 

 		while (la.kind == 30) {

 			Get();

-			ExpressionX(out e);

+			Expression(out e, true);

 			args.Add(e); 

 		}

 	}

@@ -2203,7 +2199,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (la.kind == 76) {

 			Get();

 			x = t; 

-			ExpressionX(out e);

+			Expression(out e, true);

 			Expect(77);

 			body = new List<Statement>(); 

 			while (StartOf(14)) {

@@ -2226,7 +2222,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(33);

 			e = null; 

 		} else if (StartOf(16)) {

-			ExpressionX(out ee);

+			Expression(out ee, true);

 			e = ee; 

 		} else SynErr(189);

 	}

@@ -2286,7 +2282,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

-		Expression(out e);

+		Expression(out e, false);

 		invariant = new MaybeFreeExpression(e, isFree, attrs); 

 	}

 

@@ -2318,19 +2314,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		c = new MatchCaseStmt(x, id.val, arguments, body); 

 	}

 

-	void AttributeArg(out Attributes.Argument/*!*/ arg) {

+	void AttributeArg(out Attributes.Argument arg, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e;  arg = dummyAttrArg; 

 		if (la.kind == 5) {

 			Get();

 			arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); 

 		} else if (StartOf(16)) {

-			ExpressionX(out e);

+			Expression(out e, allowSemi);

 			arg = new Attributes.Argument(t, e); 

 		} else SynErr(196);

 	}

 

-	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

-		bvars = new List<BoundVar/*!*/>();

+	void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {

+		bvars = new List<BoundVar>();

 		BoundVar/*!*/ bv;

 		attrs = null;

 		range = null;

@@ -2347,7 +2343,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		if (la.kind == 28) {

 			Get();

-			Expression(out range);

+			Expression(out range, true);

 		}

 	}

 

@@ -2363,7 +2359,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 86) {

 				Get();

 				Expect(72);

-				ExpressionX(out k);

+				Expression(out k, true);

 				Expect(73);

 			}

 			break;

@@ -2479,83 +2475,83 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(200);

 	}

 

-	void EquivExpression(out Expression/*!*/ e0) {

+	void EquivExpression(out Expression e0, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

-		ImpliesExpliesExpression(out e0);

+		ImpliesExpliesExpression(out e0, allowSemi);

 		while (la.kind == 93 || la.kind == 94) {

 			EquivOp();

 			x = t; 

-			ImpliesExpliesExpression(out e1);

+			ImpliesExpliesExpression(out e1, allowSemi);

 			e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); 

 		}

 	}

 

-	void ImpliesExpliesExpression(out Expression/*!*/ e0) {

+	void ImpliesExpliesExpression(out Expression e0, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

-		LogicalExpression(out e0);

+		LogicalExpression(out e0, allowSemi);

 		if (StartOf(25)) {

 			if (la.kind == 95 || la.kind == 96) {

 				ImpliesOp();

 				x = t; 

-				ImpliesExpression(out e1);

+				ImpliesExpression(out e1, allowSemi);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); 

 			} else {

 				ExpliesOp();

 				x = t; 

-				LogicalExpression(out e1);

+				LogicalExpression(out e1, allowSemi);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

 				while (la.kind == 97 || la.kind == 98) {

 					ExpliesOp();

 					x = t; 

-					LogicalExpression(out e1);

+					LogicalExpression(out e1, allowSemi);

 					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

 				}

 			}

 		}

 	}

 

-	void LogicalExpression(out Expression/*!*/ e0) {

+	void LogicalExpression(out Expression e0, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

-		RelationalExpression(out e0);

+		RelationalExpression(out e0, allowSemi);

 		if (StartOf(26)) {

 			if (la.kind == 99 || la.kind == 100) {

 				AndOp();

 				x = t; 

-				RelationalExpression(out e1);

+				RelationalExpression(out e1, allowSemi);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

 				while (la.kind == 99 || la.kind == 100) {

 					AndOp();

 					x = t; 

-					RelationalExpression(out e1);

+					RelationalExpression(out e1, allowSemi);

 					e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

 				}

 			} else {

 				OrOp();

 				x = t; 

-				RelationalExpression(out e1);

+				RelationalExpression(out e1, allowSemi);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

 				while (la.kind == 101 || la.kind == 102) {

 					OrOp();

 					x = t; 

-					RelationalExpression(out e1);

+					RelationalExpression(out e1, allowSemi);

 					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

 				}

 			}

 		}

 	}

 

-	void ImpliesExpression(out Expression/*!*/ e0) {

+	void ImpliesExpression(out Expression e0, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

-		LogicalExpression(out e0);

+		LogicalExpression(out e0, allowSemi);

 		if (la.kind == 95 || la.kind == 96) {

 			ImpliesOp();

 			x = t; 

-			ImpliesExpression(out e1);

+			ImpliesExpression(out e1, allowSemi);

 			e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); 

 		}

 	}

 

-	void RelationalExpression(out Expression/*!*/ e) {

+	void RelationalExpression(out Expression e, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

 		IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;

 		List<Expression> chain = null;

@@ -2569,12 +2565,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		              // 4 ("disjoint")    indicates chain of disjoint set operators

 		bool hasSeenNeq = false;

 		

-		Term(out e0);

+		Term(out e0, allowSemi);

 		e = e0; 

 		if (StartOf(27)) {

 			RelOp(out x, out op, out k);

 			firstOpTok = x; 

-			Term(out e1);

+			Term(out e1, allowSemi);

 			if (k == null) {

 			 e = new BinaryExpr(x, op, e0, e1);

 			 if (op == BinaryExpr.Opcode.Disjoint)

@@ -2636,7 +2632,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				   kind = 3;  break;

 				}

 				

-				Term(out e1);

+				Term(out e1, allowSemi);

 				ops.Add(op); prefixLimits.Add(k); chain.Add(e1);

 				if (k != null) {

 				 Contract.Assert(op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq);

@@ -2672,12 +2668,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(202);

 	}

 

-	void Term(out Expression/*!*/ e0) {

+	void Term(out Expression e0, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

-		Factor(out e0);

+		Factor(out e0, allowSemi);

 		while (la.kind == 105 || la.kind == 106) {

 			AddOp(out x, out op);

-			Factor(out e1);

+			Factor(out e1, allowSemi);

 			e0 = new BinaryExpr(x, op, e0, e1); 

 		}

 	}

@@ -2695,7 +2691,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 86) {

 				Get();

 				Expect(72);

-				ExpressionX(out k);

+				Expression(out k, true);

 				Expect(73);

 			}

 			break;

@@ -2726,7 +2722,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 86) {

 				Get();

 				Expect(72);

-				ExpressionX(out k);

+				Expression(out k, true);

 				Expect(73);

 			}

 			break;

@@ -2778,17 +2774,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

-	void Factor(out Expression/*!*/ e0) {

+	void Factor(out Expression e0, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

-		UnaryExpression(out e0);

+		UnaryExpression(out e0, allowSemi);

 		while (la.kind == 11 || la.kind == 107 || la.kind == 108) {

 			MulOp(out x, out op);

-			UnaryExpression(out e1);

+			UnaryExpression(out e1, allowSemi);

 			e0 = new BinaryExpr(x, op, e0, e1); 

 		}

 	}

 

-	void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

+	void AddOp(out IToken x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 

 		if (la.kind == 105) {

 			Get();

@@ -2799,25 +2795,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(204);

 	}

 

-	void UnaryExpression(out Expression/*!*/ e) {

+	void UnaryExpression(out Expression e, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 

 		switch (la.kind) {

 		case 106: {

 			Get();

 			x = t; 

-			UnaryExpression(out e);

+			UnaryExpression(out e, allowSemi);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

 			break;

 		}

 		case 104: case 109: {

 			NegOp();

 			x = t; 

-			UnaryExpression(out e);

+			UnaryExpression(out e, allowSemi);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

 		case 29: case 55: case 64: case 70: case 74: case 80: case 81: case 83: case 85: case 118: case 119: case 120: {

-			EndlessExpression(out e);

+			EndlessExpression(out e, allowSemi);

 			break;

 		}

 		case 1: {

@@ -2850,7 +2846,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Suffix(ref e);

 				}

 			} else if (la.kind == 1) {

-				MapComprehensionExpr(x, out e);

+				MapComprehensionExpr(x, out e, allowSemi);

 			} else if (StartOf(28)) {

 				SemErr("map must be followed by literal in brackets or comprehension."); 

 			} else SynErr(205);

@@ -2867,7 +2863,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

-	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

+	void MulOp(out IToken x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

 		if (la.kind == 11) {

 			Get();

@@ -2889,7 +2885,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(208);

 	}

 

-	void EndlessExpression(out Expression e) {

+	void EndlessExpression(out Expression e, bool allowSemi) {

 		IToken/*!*/ x;

 		Expression e0, e1;

 		Statement s;

@@ -2899,38 +2895,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		case 74: {

 			Get();

 			x = t; 

-			Expression(out e);

+			Expression(out e, true);

 			Expect(116);

-			Expression(out e0);

+			Expression(out e0, true);

 			Expect(75);

-			Expression(out e1);

+			Expression(out e1, allowSemi);

 			e = new ITEExpr(x, e, e0, e1); 

 			break;

 		}

 		case 80: {

-			MatchExpression(out e);

+			MatchExpression(out e, allowSemi);

 			break;

 		}

 		case 83: case 118: case 119: case 120: {

-			QuantifierGuts(out e);

+			QuantifierGuts(out e, allowSemi);

 			break;

 		}

 		case 55: {

-			ComprehensionExpr(out e);

+			ComprehensionExpr(out e, allowSemi);

 			break;

 		}

 		case 70: case 81: case 85: {

 			StmtInExpr(out s);

-			Expression(out e);

+			Expression(out e, allowSemi);

 			e = new StmtExpr(s.Tok, s, e); 

 			break;

 		}

 		case 29: {

-			LetExpr(out e);

+			LetExpr(out e, allowSemi);

 			break;

 		}

 		case 64: {

-			NamedExpr(out e);

+			NamedExpr(out e, allowSemi);

 			break;

 		}

 		default: SynErr(209); break;

@@ -2955,7 +2951,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Get();

 				id.val = id.val + "#";  Expression k; 

 				Expect(72);

-				ExpressionX(out k);

+				Expression(out k, true);

 				Expect(73);

 				args.Add(k); 

 			}

@@ -2969,7 +2965,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = new IdentifierSequence(idents, openParen, args); 

 	}

 

-	void Suffix(ref Expression/*!*/ e) {

+	void Suffix(ref Expression e) {

 		Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x;  List<Expression/*!*/>/*!*/ args;

 		Expression e0 = null;  Expression e1 = null;  Expression/*!*/ ee;  bool anyDots = false;

 		List<Expression> multipleIndices = null;

@@ -2984,7 +2980,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();

 					id.val = id.val + "#";  Expression k; 

 					Expect(72);

-					ExpressionX(out k);

+					Expression(out k, true);

 					Expect(73);

 					args.Add(k); 

 				}

@@ -3001,23 +2997,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; 

 			if (StartOf(16)) {

-				ExpressionX(out ee);

+				Expression(out ee, true);

 				e0 = ee; 

 				if (la.kind == 117) {

 					Get();

 					anyDots = true; 

 					if (StartOf(16)) {

-						ExpressionX(out ee);

+						Expression(out ee, true);

 						e1 = ee; 

 					}

 				} else if (la.kind == 67) {

 					Get();

-					ExpressionX(out ee);

+					Expression(out ee, true);

 					e1 = ee; 

 				} else if (la.kind == 30 || la.kind == 73) {

 					while (la.kind == 30) {

 						Get();

-						ExpressionX(out ee);

+						Expression(out ee, true);

 						if (multipleIndices == null) {

 						 multipleIndices = new List<Expression>();

 						 multipleIndices.Add(e0);

@@ -3030,7 +3026,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Get();

 				anyDots = true; 

 				if (StartOf(16)) {

-					ExpressionX(out ee);

+					Expression(out ee, true);

 					e1 = ee; 

 				}

 			} else SynErr(211);

@@ -3102,7 +3098,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 10) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			ExpressionX(out e);

+			Expression(out e, true);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(33);

 		} else if (StartOf(29)) {

@@ -3123,10 +3119,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(73);

 	}

 

-	void MapComprehensionExpr(IToken/*!*/ mapToken, out Expression e) {

+	void MapComprehensionExpr(IToken mapToken, out Expression e, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

-		BoundVar/*!*/ bv;

-		List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

+		BoundVar bv;

+		List<BoundVar> bvars = new List<BoundVar>();

 		Expression range = null;

 		Expression body;

 		

@@ -3134,15 +3130,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		bvars.Add(bv); 

 		if (la.kind == 28) {

 			Get();

-			Expression(out range);

+			Expression(out range, true);

 		}

 		QSep();

-		Expression(out body);

+		Expression(out body, allowSemi);

 		e = new MapComprehension(mapToken, bvars, range ?? new LiteralExpr(mapToken, true), body);

 		

 	}

 

-	void ConstAtomExpression(out Expression/*!*/ e) {

+	void ConstAtomExpression(out Expression e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

 		IToken/*!*/ x;  BigInteger n;

 		e = dummyExpr;

@@ -3177,7 +3173,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; 

 			Expect(10);

-			Expression(out e);

+			Expression(out e, true);

 			Expect(33);

 			e = new FreshExpr(x, e); 

 			break;

@@ -3186,7 +3182,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			x = t; 

 			Expect(10);

-			Expression(out e);

+			Expression(out e, true);

 			Expect(33);

 			e = new OldExpr(x, e); 

 			break;

@@ -3194,7 +3190,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		case 28: {

 			Get();

 			x = t; 

-			Expression(out e);

+			Expression(out e, true);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); 

 			Expect(28);

 			break;

@@ -3202,7 +3198,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		case 10: {

 			Get();

 			x = t; 

-			Expression(out e);

+			Expression(out e, true);

 			e = new ParensExpression(x, e); 

 			Expect(33);

 			break;

@@ -3238,15 +3234,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void MapLiteralExpressions(out List<ExpressionPair> elements) {

 		Expression/*!*/ d, r;

 		elements = new List<ExpressionPair/*!*/>(); 

-		ExpressionX(out d);

+		Expression(out d, true);

 		Expect(67);

-		ExpressionX(out r);

+		Expression(out r, true);

 		elements.Add(new ExpressionPair(d,r)); 

 		while (la.kind == 30) {

 			Get();

-			ExpressionX(out d);

+			Expression(out d, true);

 			Expect(67);

-			ExpressionX(out r);

+			Expression(out r, true);

 			elements.Add(new ExpressionPair(d,r)); 

 		}

 	}

@@ -3259,21 +3255,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(217);

 	}

 

-	void MatchExpression(out Expression/*!*/ e) {

+	void MatchExpression(out Expression e, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

 		

 		Expect(80);

 		x = t; 

-		Expression(out e);

+		Expression(out e, allowSemi);

 		while (la.kind == 76) {

-			CaseExpression(out c);

+			CaseExpression(out c, allowSemi);

 			cases.Add(c); 

 		}

 		e = new MatchExpr(x, e, cases); 

 	}

 

-	void QuantifierGuts(out Expression/*!*/ q) {

+	void QuantifierGuts(out Expression q, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;

 		bool univ = false;

 		List<BoundVar/*!*/> bvars;

@@ -3290,7 +3286,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(218);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

-		Expression(out body);

+		Expression(out body, allowSemi);

 		if (univ) {

 		 q = new ForallExpr(x, bvars, range, body, attrs);

 		} else {

@@ -3299,12 +3295,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 	}

 

-	void ComprehensionExpr(out Expression/*!*/ q) {

+	void ComprehensionExpr(out Expression q, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out q) != null);

-		IToken/*!*/ x = Token.NoToken;

-		BoundVar/*!*/ bv;

-		List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

-		Expression/*!*/ range;

+		IToken x = Token.NoToken;

+		BoundVar bv;

+		List<BoundVar/*!*/> bvars = new List<BoundVar>();

+		Expression range;

 		Expression body = null;

 		

 		Expect(55);

@@ -3317,10 +3313,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			bvars.Add(bv); 

 		}

 		Expect(28);

-		Expression(out range);

+		Expression(out range, allowSemi);

 		if (la.kind == 121 || la.kind == 122) {

 			QSep();

-			Expression(out body);

+			Expression(out body, allowSemi);

 		}

 		if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }

 		q = new SetComprehension(x, bvars, range, body);

@@ -3338,7 +3334,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(219);

 	}

 

-	void LetExpr(out Expression e) {

+	void LetExpr(out Expression e, bool allowSemi) {

 		IToken/*!*/ x;

 		e = dummyExpr;

 		BoundVar d;

@@ -3362,19 +3358,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			exact = false; 

 		} else SynErr(220);

-		Expression(out e);

+		Expression(out e, false);

 		letRHSs.Add(e); 

 		while (la.kind == 30) {

 			Get();

-			Expression(out e);

+			Expression(out e, false);

 			letRHSs.Add(e); 

 		}

 		Expect(7);

-		Expression(out e);

+		Expression(out e, allowSemi);

 		e = new LetExpr(x, letVars, letRHSs, e, exact); 

 	}

 

-	void NamedExpr(out Expression e) {

+	void NamedExpr(out Expression e, bool allowSemi) {

 		IToken/*!*/ x, d;

 		e = dummyExpr;

 		Expression expr;

@@ -3383,12 +3379,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		x = t; 

 		NoUSIdent(out d);

 		Expect(6);

-		Expression(out e);

+		Expression(out e, allowSemi);

 		expr = e;

 		e = new NamedExpr(x, d.val, expr); 

 	}

 

-	void CaseExpression(out MatchCaseExpr/*!*/ c) {

+	void CaseExpression(out MatchCaseExpr c, bool allowSemi) {

 		Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id;

 		List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();

 		BoundVar/*!*/ bv;

@@ -3409,7 +3405,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(33);

 		}

 		Expect(77);

-		Expression(out body);

+		Expression(out body, allowSemi);

 		c = new MatchCaseExpr(x, id.val, arguments, body); 

 	}

 

@@ -3438,11 +3434,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(1);

 		aName = t.val; 

 		if (StartOf(30)) {

-			AttributeArg(out aArg);

+			AttributeArg(out aArg, true);

 			aArgs.Add(aArg); 

 			while (la.kind == 30) {

 				Get();

-				AttributeArg(out aArg);

+				AttributeArg(out aArg, true);

 				aArgs.Add(aArg); 

 			}

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index c48b0c61..d9d6adcd 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -31,7 +31,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       using (var wr = new System.IO.StringWriter()) {

         var pr = new Printer(wr);

-        pr.PrintExpression(expr);

+        pr.PrintExpression(expr, true);

         return wr.ToString();

       }

     }

@@ -276,13 +276,13 @@ namespace Microsoft.Dafny {
         wr.Write(" {{:{0}", a.Name);

         if (a.Args != null)

         {

-          PrintAttributeArgs(a.Args);

+          PrintAttributeArgs(a.Args, false);

         }

         wr.Write("}");

       }

     }

 

-    public void PrintAttributeArgs(List<Attributes.Argument> args) {

+    public void PrintAttributeArgs(List<Attributes.Argument> args, bool isFollowedBySemicolon) {

       Contract.Requires(args != null);

       string prefix = " ";

       foreach (Attributes.Argument arg in args) {

@@ -293,7 +293,7 @@ namespace Microsoft.Dafny {
           wr.Write("\"{0}\"", arg.S);

         } else {

           Contract.Assert( arg.E != null);

-          PrintExpression(arg.E);

+          PrintExpression(arg.E, isFollowedBySemicolon);

         }

       }

     }

@@ -350,7 +350,7 @@ namespace Microsoft.Dafny {
       if (f.Body != null) {

         Indent(indent);

         wr.WriteLine("{");

-        PrintExtendedExpr(f.Body, ind, true, false);

+        PrintExtendedExpr(f.Body, ind, true, false, false);

         Indent(indent);

         wr.WriteLine("}");

       }

@@ -449,7 +449,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(e != null);

         Indent(indent);

         wr.Write("{0} ", kind);

-        PrintExpression(e);

+        PrintExpression(e, true);

         wr.WriteLine(";");

       }

     }

@@ -464,7 +464,7 @@ namespace Microsoft.Dafny {
           PrintAttributes(decs.Attributes);

         }

         wr.Write(" ");

-        PrintExpressionList(decs.Expressions);

+        PrintExpressionList(decs.Expressions, true);

         wr.WriteLine(";");

       }

     }

@@ -499,7 +499,7 @@ namespace Microsoft.Dafny {
         }

 

         wr.Write(" ");

-        PrintExpression(e.E);

+        PrintExpression(e.E, true);

 

         wr.WriteLine(";");

       }

@@ -544,13 +544,13 @@ namespace Microsoft.Dafny {
           PrintAttributes(stmt.Attributes);

         }

         wr.Write(" ");

-        PrintExpression(expr);

+        PrintExpression(expr, true);

         wr.Write(";");

 

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         wr.Write("print");

-        PrintAttributeArgs(s.Args);

+        PrintAttributeArgs(s.Args, true);

         wr.Write(";");

 

       } else if (stmt is BreakStmt) {

@@ -581,7 +581,7 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

-        PrintExpression(s.Lhs);

+        PrintExpression(s.Lhs, true);

         wr.Write(" := ");

         PrintRhs(s.Rhs);

         wr.Write(";");

@@ -606,13 +606,13 @@ namespace Microsoft.Dafny {
           string sep = "";

           foreach (IdentifierExpr v in s.Lhs) {

             wr.Write(sep);

-            PrintExpression(v);

+            PrintExpression(v, true);

             sep = ", ";

           }

           wr.Write(" := ");

         }

         if (!(s.Receiver is ImplicitThisExpr)) {

-          PrintExpr(s.Receiver, 0x70, false, false, -1);

+          PrintExpr(s.Receiver, 0x70, false, false, true, -1);

           wr.Write(".");

         }

         wr.Write("{0}", s.MethodName);

@@ -693,7 +693,7 @@ namespace Microsoft.Dafny {
           var h = s.Hints[i];

           // print the line

           Indent(lineInd);

-          PrintExpression(e, lineInd);

+          PrintExpression(e, true, lineInd);

           wr.WriteLine(";");

           if (i == hintCount) {

             break;

@@ -717,7 +717,7 @@ namespace Microsoft.Dafny {
       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         wr.Write("match ");

-        PrintExpression(s.Source);

+        PrintExpression(s.Source, false);

         wr.WriteLine(" {");

         int caseInd = indent + IndentAmount;

         foreach (MatchCaseStmt mc in s.Cases) {

@@ -746,7 +746,7 @@ namespace Microsoft.Dafny {
         string sep = "";

         foreach (var lhs in s.Lhss) {

           wr.Write(sep);

-          PrintExpression(lhs);

+          PrintExpression(lhs, true);

           sep = ", ";

         }

         PrintUpdateRHS(s);

@@ -819,7 +819,7 @@ namespace Microsoft.Dafny {
         if (update.AssumeToken != null) {

           wr.Write("assume ");

         }

-        PrintExpression(update.Expr);

+        PrintExpression(update.Expr, true);

       } else {

         Contract.Assert(s == null);  // otherwise, unknown type

       }

@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
       foreach (var alternative in alternatives) {

         Indent(caseInd);

         wr.Write("case ");

-        PrintExpression(alternative.Guard);

+        PrintExpression(alternative.Guard, false);

         wr.WriteLine(" =>");

         foreach (Statement s in alternative.Body) {

           Indent(caseInd + IndentAmount);

@@ -889,7 +889,7 @@ namespace Microsoft.Dafny {
     void PrintRhs(AssignmentRhs rhs) {

       Contract.Requires(rhs != null);

       if (rhs is ExprRhs) {

-        PrintExpression(((ExprRhs)rhs).Expr);

+        PrintExpression(((ExprRhs)rhs).Expr, true);

       } else if (rhs is HavocRhs) {

         wr.Write("*");

       } else if (rhs is TypeRhs) {

@@ -901,7 +901,7 @@ namespace Microsoft.Dafny {
           foreach (Expression dim in t.ArrayDimensions) {

             Contract.Assume(dim != null);

             wr.Write(s);

-            PrintExpression(dim);

+            PrintExpression(dim, false);

             s = ", ";

           }

           wr.Write("]");

@@ -912,13 +912,13 @@ namespace Microsoft.Dafny {
             wr.Write(".{0}", t.OptionalNameComponent);

           }

           wr.Write("(");

-          PrintExpressionList(t.Arguments);

+          PrintExpressionList(t.Arguments, false);

           wr.Write(")");

         }

       } else if (rhs is CallRhs) {

         var r = (CallRhs)rhs;

         if (!(r.Receiver is ImplicitThisExpr)) {

-          PrintExpr(r.Receiver, 0x70, false, false, -1);

+          PrintExpr(r.Receiver, 0x70, false, false, true, -1);

           wr.Write(".");

         }

         wr.Write("{0}", r.MethodName);

@@ -937,7 +937,7 @@ namespace Microsoft.Dafny {
       if (guard == null) {

         wr.Write("*");

       } else {

-        PrintExpression(guard);

+        PrintExpression(guard, false);

       }

     }

 

@@ -946,30 +946,30 @@ namespace Microsoft.Dafny {
       wr.Write(op.ToString());

       if (op is CalcStmt.TernaryCalcOp) {

         wr.Write("[");

-        PrintExpression(((CalcStmt.TernaryCalcOp) op).Index);

+        PrintExpression(((CalcStmt.TernaryCalcOp) op).Index, false);

         wr.Write("]");

       }

     }

 

     // ----------------------------- PrintExpression -----------------------------

 

-    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {

+    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen, bool isFollowedBySemicolon) {

       Contract.Requires(expr != null);

       Indent(indent);

       if (expr is ITEExpr) {

         while (true) {

           ITEExpr ite = (ITEExpr)expr;

           wr.Write("if ");

-          PrintExpression(ite.Test);

+          PrintExpression(ite.Test, false);

           wr.WriteLine(" then");

-          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);

+          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false, false);

           expr = ite.Els;

           if (expr is ITEExpr) {

             Indent(indent);  wr.Write("else ");

           } else {

             Indent(indent);  wr.WriteLine("else");

             Indent(indent + IndentAmount);

-            PrintExpression(expr);

+            PrintExpression(expr, isFollowedBySemicolon);

             wr.WriteLine(endWithCloseParen ? ")" : "");

             return;

           }

@@ -977,7 +977,7 @@ namespace Microsoft.Dafny {
       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         wr.Write("match ");

-        PrintExpression(me.Source);

+        PrintExpression(me.Source, isFollowedBySemicolon);

         wr.WriteLine();

         int i = 0;

         foreach (MatchCaseExpr mc in me.Cases) {

@@ -998,34 +998,34 @@ namespace Microsoft.Dafny {
           } else {

             wr.WriteLine(" =>");

           }

-          PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, parensNeeded || (isLastCase && endWithCloseParen));

+          PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, parensNeeded || (isLastCase && endWithCloseParen), !parensNeeded && isFollowedBySemicolon);

           i++;

         }

       } else if (expr is ParensExpression) {

-        PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen);

+        PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen, isFollowedBySemicolon);

       } else {

-        PrintExpression(expr, indent);

+        PrintExpression(expr, isFollowedBySemicolon, indent);

         wr.WriteLine(endWithCloseParen ? ")" : "");

       }

     }

 

-    public void PrintExpression(Expression expr) {

+    public void PrintExpression(Expression expr, bool isFollowedBySemicolon) {

       Contract.Requires(expr != null);

-      PrintExpr(expr, 0, false, true, -1);

+      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, - 1);

     }

 

     /// <summary>

     /// An indent of -1 means print the entire expression on one line.

     /// </summary>

-    public void PrintExpression(Expression expr, int indent) {

+    public void PrintExpression(Expression expr, bool isFollowedBySemicolon, int indent) {

       Contract.Requires(expr != null);

-      PrintExpr(expr, 0, false, true, indent);

+      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, indent);

     }

 

     /// <summary>

     /// An indent of -1 means print the entire expression on one line.

     /// </summary>

-    void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, bool isRightmost, int indent)

+    void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, bool isRightmost, bool isFollowedBySemicolon, int indent)

     {

       Contract.Requires(-1 <= indent);

       Contract.Requires(expr != null);

@@ -1054,7 +1054,7 @@ namespace Microsoft.Dafny {
         wr.Write("#{0}.{1}", dtv.DatatypeName, dtv.MemberName);

         if (dtv.Arguments.Count != 0) {

           wr.Write("(");

-          PrintExpressionList(dtv.Arguments);

+          PrintExpressionList(dtv.Arguments, false);

           wr.Write(")");

         }

 

@@ -1062,7 +1062,7 @@ namespace Microsoft.Dafny {
         DisplayExpression e = (DisplayExpression)expr;

         if (e is MultiSetDisplayExpr) wr.Write("multiset");

         wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");

-        PrintExpressionList(e.Elements);

+        PrintExpressionList(e.Elements, false);

         wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");

 

       } else if (expr is MapDisplayExpr) {

@@ -1081,7 +1081,7 @@ namespace Microsoft.Dafny {
 

         if (parensNeeded) { wr.Write("("); }

         if (!(e.Obj is ImplicitThisExpr)) {

-          PrintExpr(e.Obj, opBindingStrength, false, false, -1);

+          PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

           wr.Write(".");

         }

         wr.Write(e.SuffixName);

@@ -1097,7 +1097,7 @@ namespace Microsoft.Dafny {
 

         if (parensNeeded) { wr.Write("("); }

         if (!(e.Obj is ImplicitThisExpr)) {

-          PrintExpr(e.Obj, opBindingStrength, false, false, -1);

+          PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

           wr.Write(".");

         }

         wr.Write(e.FieldName);

@@ -1111,18 +1111,18 @@ namespace Microsoft.Dafny {
           (fragileContext && opBindingStrength == contextBindingStrength);

 

         if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Seq, 0x00, false, false, indent);  // BOGUS: fix me

+        PrintExpr(e.Seq, 0x00, false, false, !parensNeeded && isFollowedBySemicolon, indent);  // BOGUS: fix me

         wr.Write("[");

         if (e.SelectOne) {

           Contract.Assert( e.E0 != null);

-          PrintExpression(e.E0);

+          PrintExpression(e.E0, false);

         } else {

           if (e.E0 != null) {

-            PrintExpression(e.E0);

+            PrintExpression(e.E0, false);

           }

           wr.Write(e.E0 != null && e.E1 != null ? " .. " : "..");

           if (e.E1 != null) {

-            PrintExpression(e.E1);

+            PrintExpression(e.E1, false);

           }

         }

         wr.Write("]");

@@ -1136,12 +1136,12 @@ namespace Microsoft.Dafny {
           (fragileContext && opBindingStrength == contextBindingStrength);

 

         if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Array, 0x00, false, false, indent);  // BOGUS: fix me

+        PrintExpr(e.Array, 0x00, false, false, !parensNeeded && isFollowedBySemicolon, indent);  // BOGUS: fix me

         string prefix = "[";

         foreach (Expression idx in e.Indices) {

           Contract.Assert(idx != null);

           wr.Write(prefix);

-          PrintExpression(idx);

+          PrintExpression(idx, false);

           prefix = ", ";

         }

         wr.Write("]");

@@ -1155,11 +1155,11 @@ namespace Microsoft.Dafny {
           (fragileContext && opBindingStrength == contextBindingStrength);

 

         if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Seq, 00, false, false, indent);  // BOGUS: fix me

+        PrintExpr(e.Seq, 00, false, false, !parensNeeded && isFollowedBySemicolon, indent);  // BOGUS: fix me

         wr.Write("[");

-        PrintExpression(e.Index);

+        PrintExpression(e.Index, false);

         wr.Write(" := ");

-        PrintExpression(e.Value);

+        PrintExpression(e.Value, false);

         wr.Write("]");

         if (parensNeeded) { wr.Write(")"); }

 

@@ -1173,7 +1173,7 @@ namespace Microsoft.Dafny {
 

         if (parensNeeded) { wr.Write("("); }

         if (!(e.Receiver is ImplicitThisExpr)) {

-          PrintExpr(e.Receiver, opBindingStrength, false, false, -1);

+          PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

           wr.Write(".");

         }

         wr.Write(e.Name);

@@ -1185,24 +1185,24 @@ namespace Microsoft.Dafny {
 

       } else if (expr is OldExpr) {

         wr.Write("old(");

-        PrintExpression(((OldExpr)expr).E);

+        PrintExpression(((OldExpr)expr).E, false);

         wr.Write(")");

 

       } else if (expr is MultiSetFormingExpr) {

         wr.Write("multiset(");

-        PrintExpression(((MultiSetFormingExpr)expr).E);

+        PrintExpression(((MultiSetFormingExpr)expr).E, false);

         wr.Write(")");

 

       } else if (expr is FreshExpr) {

         wr.Write("fresh(");

-        PrintExpression(((FreshExpr)expr).E);

+        PrintExpression(((FreshExpr)expr).E, false);

         wr.Write(")");

 

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         if (e.Op == UnaryExpr.Opcode.SeqLength) {

           wr.Write("|");

-          PrintExpression(e.E);

+          PrintExpression(e.E, false);

           wr.Write("|");

         } else {

           // Prefix operator.

@@ -1224,7 +1224,7 @@ namespace Microsoft.Dafny {
 

           if (parensNeeded) { wr.Write("("); }

           wr.Write(op);

-          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, -1);

+          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);

           if (parensNeeded) { wr.Write(")"); }

         }

 

@@ -1275,31 +1275,32 @@ namespace Microsoft.Dafny {
 

         string op = BinaryExpr.OpcodeString(e.Op);

         if (parensNeeded) { wr.Write("("); }

+        var sem = !parensNeeded && isFollowedBySemicolon;

         if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, indent);

+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);

           wr.WriteLine(" {0}", op);

           Indent(indent);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, indent);

+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, indent);

         } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, indent);

+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);

           wr.WriteLine(" {0}", op);

           int ind = indent + IndentAmount;

           Indent(ind);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, ind);

+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);

         } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Exp) {

-          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, indent);

+          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, indent);

           wr.WriteLine(" {0}", op);

           int ind = indent + IndentAmount;

           Indent(ind);

-          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, ind);

+          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);

         } else if (e.Op == BinaryExpr.Opcode.Exp) {

-          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, -1);

+          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);

           wr.Write(" {0} ", op);

-          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, -1);

+          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);

         } else {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, -1);

+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, -1);

           wr.Write(" {0} ", op);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, -1);

+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);

         }

         if (parensNeeded) { wr.Write(")"); }

 

@@ -1318,11 +1319,12 @@ namespace Microsoft.Dafny {
               (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

 

             if (parensNeeded) { wr.Write("("); }

-            PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, -1);

+            var sem = !parensNeeded && isFollowedBySemicolon;

+            PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);

             wr.Write(" {0}#[", e.Op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=");

-            PrintExpression(e.E0);

+            PrintExpression(e.E0, false);

             wr.Write("] ");

-            PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, -1);

+            PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);

             if (parensNeeded) { wr.Write(")"); }

             break;

           default:

@@ -1340,17 +1342,18 @@ namespace Microsoft.Dafny {
           (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

 

         if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Operands[0], opBindingStrength, true, false, -1);

+        var sem = !parensNeeded && isFollowedBySemicolon;

+        PrintExpr(e.Operands[0], opBindingStrength, true, false, sem, -1);

         for (int i = 0; i < e.Operators.Count; i++) {

           string op = BinaryExpr.OpcodeString(e.Operators[i]);

           if (e.PrefixLimits[i] == null) {

             wr.Write(" {0} ", op);

           } else {

             wr.Write(" {0}#[", op);

-            PrintExpression(e.PrefixLimits[i]);

+            PrintExpression(e.PrefixLimits[i], false);

             wr.Write("] ");

           }

-          PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), -1);

+          PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), sem, -1);

         }

         if (parensNeeded) { wr.Write(")"); }

 

@@ -1370,12 +1373,11 @@ namespace Microsoft.Dafny {
         } else {

           wr.Write(" :| ");

         }

-        PrintExpressionList(e.RHSs);

+        PrintExpressionList(e.RHSs, true);

         wr.Write("; ");

-        PrintExpression(e.Body);

+        PrintExpression(e.Body, !parensNeeded && isFollowedBySemicolon);

         if (parensNeeded) { wr.Write(")"); }

 

-

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         bool parensNeeded = !isRightmost;

@@ -1387,16 +1389,16 @@ namespace Microsoft.Dafny {
           int ind = indent + IndentAmount;

           wr.WriteLine();

           Indent(ind);

-          PrintExpression(e.Term, ind);

+          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon, ind);

         } else {

-          PrintExpression(e.Term);

+          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

         }

         if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is NamedExpr) {

         var e = (NamedExpr)expr;

         wr.Write("expr {0}: ", e.Name);

-        PrintExpression(e.Body);

+        PrintExpression(e.Body, isFollowedBySemicolon);

 

        } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

@@ -1411,10 +1413,10 @@ namespace Microsoft.Dafny {
         }

         PrintAttributes(e.Attributes);

         wr.Write(" | ");

-        PrintExpression(e.Range);

+        PrintExpression(e.Range, !parensNeeded && isFollowedBySemicolon);

         if (!e.TermIsImplicit) {

           wr.Write(" :: ");

-          PrintExpression(e.Term);

+          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

         }

         if (parensNeeded) { wr.Write(")"); }

 

@@ -1431,9 +1433,9 @@ namespace Microsoft.Dafny {
         }

         PrintAttributes(e.Attributes);

         wr.Write(" | ");

-        PrintExpression(e.Range);

+        PrintExpression(e.Range, !parensNeeded && isFollowedBySemicolon);

         wr.Write(" :: ");

-        PrintExpression(e.Term);

+        PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

         if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is WildcardExpr) {

@@ -1441,11 +1443,17 @@ namespace Microsoft.Dafny {
 

       } else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

-        bool parensNeeded = !isRightmost;

+        bool parensNeeded;

+        if (e.S is AssertStmt || e.S is AssumeStmt || e.S is CalcStmt) {

+          parensNeeded = !isRightmost;

+        } else {

+          parensNeeded = !isRightmost || isFollowedBySemicolon;

+        }

         if (parensNeeded) { wr.Write("("); }

         int ind = indent < 0 ? IndentAmount : indent;  // if the expression was to be printed on one line, instead print the .S part at indentation IndentAmount (not pretty, but something)

         PrintStatement(e.S, ind);

-        PrintExpression(e.E);

+        wr.Write(" ");

+        PrintExpression(e.E, !parensNeeded && isFollowedBySemicolon);

         if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is ITEExpr) {

@@ -1453,17 +1461,17 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !isRightmost;

         if (parensNeeded) { wr.Write("("); }

         wr.Write("if ");

-        PrintExpression(ite.Test);

+        PrintExpression(ite.Test, false);

         wr.Write(" then ");

-        PrintExpression(ite.Thn);

+        PrintExpression(ite.Thn, false);

         wr.Write(" else ");

-        PrintExpression(ite.Els);

+        PrintExpression(ite.Els, !parensNeeded && isFollowedBySemicolon);

         if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

         // printing of parentheses is done optimally, not according to the parentheses in the given program

-        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);

+        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);

 

       } else if (expr is IdentifierSequence) {

         var e = (IdentifierSequence)expr;

@@ -1483,7 +1491,7 @@ namespace Microsoft.Dafny {
       } else if (expr is BoxingCastExpr) {

         // this is not expected for a parsed program, but we may be called for /trace purposes in the translator

         var e = (BoxingCastExpr)expr;

-        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);

+        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);

       } else if (expr is Translator.BoogieWrapper) {

         wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here

       } else {

@@ -1502,7 +1510,7 @@ namespace Microsoft.Dafny {
       PrintAttributes(attrs);

       if (range != null) {

         wr.Write(" | ");

-        PrintExpression(range);

+        PrintExpression(range, false);

       }

     }

 

@@ -1511,23 +1519,23 @@ namespace Microsoft.Dafny {
       Contract.Requires(name != null);

       if (name.EndsWith("#")) {

         wr.Write("[");

-        PrintExpression(args[0]);

+        PrintExpression(args[0], false);

         wr.Write("]");

         args = new List<Expression>(args.Skip(1));

       }

       wr.Write("(");

-      PrintExpressionList(args);

+      PrintExpressionList(args, false);

       wr.Write(")");

     }

 

-    void PrintExpressionList(List<Expression> exprs) {

+    void PrintExpressionList(List<Expression> exprs, bool isFollowedBySemicolon) {

       Contract.Requires(exprs != null);

       string sep = "";

       foreach (Expression e in exprs) {

         Contract.Assert(e != null);

         wr.Write(sep);

         sep = ", ";

-        PrintExpression(e);

+        PrintExpression(e, isFollowedBySemicolon);

       }

     }

     void PrintExpressionPairList(List<ExpressionPair> exprs) {

@@ -1537,9 +1545,9 @@ namespace Microsoft.Dafny {
         Contract.Assert(p != null);

         wr.Write(sep);

         sep = ", ";

-        PrintExpression(p.A);

+        PrintExpression(p.A, false);

         wr.Write(":=");

-        PrintExpression(p.B);

+        PrintExpression(p.B, false);

       }

     }

 

@@ -1550,7 +1558,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(fe != null);

         wr.Write(sep);

         sep = ", ";

-        PrintExpression(fe.E);

+        PrintExpression(fe.E, true);

         if (fe.FieldName != null) {

           wr.Write("`{0}", fe.FieldName);

         }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index be48e23a..56711ff6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -360,16 +360,14 @@ namespace Microsoft.Dafny
             }

             if (showIt) {

               s += "decreases ";

-              if (m.Decreases.Expressions.Count == 0) {

-                s += ";";  // found nothing; indicate this more explicitly by just showing a semi-colon

-              } else {

+              if (m.Decreases.Expressions.Count != 0) {

                 string sep = "";

                 foreach (var d in m.Decreases.Expressions) {

                   s += sep + Printer.ExprToString(d);

                   sep = ", ";

                 }

-                // don't bother with a terminating semi-colon

               }

+              s += ";";  // always terminate with a semi-colon, even in the case of an empty decreases clause

               // Note, in the following line, we use the location information for "clbl", not "m".  These

               // are the same, except in the case where "clbl" is a CoMethod and "m" is a prefix method.

               ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length);

@@ -4447,15 +4445,14 @@ namespace Microsoft.Dafny
       }

       if (loopStmt.InferredDecreases) {

         string s = "decreases ";

-        if (theDecreases.Count == 0) {

-          s += ";";  // found nothing; indicate this more explicitly by just showing a semi-colon

-        } else {

+        if (theDecreases.Count != 0) {

           string sep = "";

           foreach (var d in theDecreases) {

             s += sep + Printer.ExprToString(d);

             sep = ", ";

           }

         }

+        s += ";";  // always terminate with a semi-colon, even in the case of an empty decreases clause

         ReportAdditionalInformation(loopStmt.Tok, s, loopStmt.Tok.val.Length);

       }

     }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a9546227..dec1302f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2525,7 +2525,7 @@ namespace Microsoft.Dafny {
       using (var writer = new System.IO.StringWriter())

       {

         var printer = new Printer(writer);

-        printer.PrintExtendedExpr(e, 0, false, false);

+        printer.PrintExtendedExpr(e, 0, false, false, true);

         data = Encoding.UTF8.GetBytes(writer.ToString());

       }

 

@@ -2550,7 +2550,7 @@ namespace Microsoft.Dafny {
         printer.PrintDecreasesSpec(f.Decreases, 0);

         if (!specificationOnly && f.Body != null)

         {

-          printer.PrintExtendedExpr(f.Body, 0, false, false);

+          printer.PrintExtendedExpr(f.Body, 0, false, false, true);

         }

         data = Encoding.UTF8.GetBytes(writer.ToString());

       }

@@ -9783,7 +9783,7 @@ namespace Microsoft.Dafny {
 

     List<BoundVar> ApplyInduction(QuantifierExpr e) {

       return ApplyInduction(e.BoundVars, e.Attributes, new List<Expression>() { e.LogicalBody() },

-        delegate(System.IO.TextWriter wr) { new Printer(Console.Out).PrintExpression(e); });

+        delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); });

     }

 

     delegate void TracePrinter(System.IO.TextWriter wr);

@@ -10688,7 +10688,10 @@ namespace Microsoft.Dafny {
           r = rr;

         } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          r = new CalcStmt(s.Tok, s.EndTok, SubstCalcOp(s.Op), s.Lines.ConvertAll(Substitute), s.Hints.ConvertAll(SubstBlockStmt), s.StepOps.ConvertAll(SubstCalcOp), SubstCalcOp(s.ResultOp));

+          var rr = new CalcStmt(s.Tok, s.EndTok, SubstCalcOp(s.Op), s.Lines.ConvertAll(Substitute), s.Hints.ConvertAll(SubstBlockStmt), s.StepOps.ConvertAll(SubstCalcOp), SubstCalcOp(s.ResultOp));

+          rr.Steps.AddRange(s.Steps.ConvertAll(Substitute));

+          rr.Result = Substitute(s.Result);

+          r = rr;

         } else if (stmt is MatchStmt) {

           var s = (MatchStmt)stmt;

           var rr = new MatchStmt(s.Tok, s.EndTok, Substitute(s.Source), s.Cases.ConvertAll(SubstMatchCaseStmt));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 045900ae..1c5ecf49 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1257,8 +1257,12 @@ StatementExpressions.dfy(85,5): Error: value assigned to a nat must be non-negat
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

+StatementExpressions.dfy(95,11): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 13 verified, 4 errors

+Dafny program verifier finished with 17 verified, 5 errors

 

 -------------------- Coinductive.dfy --------------------

 Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed

diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy
index 386d030b..99416013 100644
--- a/Test/dafny0/StatementExpressions.dfy
+++ b/Test/dafny0/StatementExpressions.dfy
@@ -85,3 +85,74 @@ function F_PreconditionViolation(n: int): int
   L(n);  // error: argument might be negative

   50 / Fact(n)

 }

+

+// --------------------- These had had parsing problems in the past

+

+lemma MyLemma(x: int) {

+  var d: Dtz;

+  if 0 < x {

+    var y: int;

+    match MyLemma(y); d {  // error: cannot prove termination

+      case Cons0(_) =>

+      case Cons1(_) =>

+    }

+  }

+}

+

+function Parsing_Regression_test0(): int

+{

+  var x := 12;

+  assert x < 20;

+  MyLemma(x);

+  calc { x; < x+1; }

+  // and again

+  var x := 12;

+  assert x < 20;

+  MyLemma(x);

+  calc { x; < x+1; }

+  17

+}

+

+datatype Dtz = Cons0(int) | Cons1(bool)

+

+function Parsing_Regression_test1(dtz: Dtz): int

+{

+  match dtz

+  case Cons0(s) =>

+    var x := 12;

+    assert x < 20;

+    MyLemma(x);

+    calc { x; < x+1; }

+    // and again

+    var x := 12;

+    assert x < 20;

+    MyLemma(x);

+    calc { x; < x+1; }

+    17

+  case Cons1(_) =>

+    var x := 12;

+    assert x < 20;

+    MyLemma(x);

+    calc { x; < x+1; }

+    // and again

+    var x := 12;

+    assert x < 20;

+    MyLemma(x);

+    calc { x; < x+1; }

+    19

+}

+

+function Parsing_Regression_test2(): int

+{

+  // parentheses should be allowed anywhere

+  var x := 12;

+  ( assert x < 20;

+    ( MyLemma(x);

+      ( calc { x; < x+1; }

+        ( var x := 12;

+          ( assert x < 20;

+            ( MyLemma(x);

+              ( calc { x; < x+1; }

+                17

+  ) ) ) ) ) ) )

+}