From 119eaf59418889d83fb57c3669f5095893262ba3 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Wed, 13 Jun 2012 17:44:45 -0700
Subject: Dafny: Changed the semantics of the assign-such-that statement "x :|
 P;" to check the existence of a value.  The previous "assume only" version is
 available by supplying the keyword "assume" in front of "P".

---
 Source/Dafny/Compiler.cs              |  15 +++-
 Source/Dafny/Dafny.atg                |  10 ++-
 Source/Dafny/DafnyAst.cs              |  32 ++++++-
 Source/Dafny/Parser.cs                | 154 ++++++++++++++++++----------------
 Source/Dafny/Printer.cs               |   5 +-
 Source/Dafny/RefinementTransformer.cs |   4 +-
 Source/Dafny/Resolver.cs              |  16 +++-
 Source/Dafny/Scanner.cs               |  26 +++---
 Source/Dafny/Translator.cs            |  36 +++++++-
 9 files changed, 200 insertions(+), 98 deletions(-)

(limited to 'Source/Dafny')

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 58c73561..911e5aac 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -838,7 +838,10 @@ namespace Microsoft.Dafny {
       if (stmt is AssumeStmt) {
         Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);
       } else if (stmt is AssignSuchThatStmt) {
-        Error("an assign-such-that statement cannot be compiled (line {0})", stmt.Tok.line);
+        var s = (AssignSuchThatStmt)stmt;
+        if (s.AssumeToken != null) {
+          Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
+        }
       } else {
         foreach (var ss in stmt.SubStatements) {
           CheckHasNoAssumes(ss);
@@ -914,6 +917,16 @@ namespace Microsoft.Dafny {
         Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne);  // multi-element array assignments are not allowed
         TrRhs(null, s.Lhs, s.Rhs, indent);
 
+      } else if (stmt is AssignSuchThatStmt) {
+        var s = (AssignSuchThatStmt)stmt;
+        foreach (var lhs in s.Lhss) {
+          // assigning to a local ghost variable or to a ghost field is okay
+          if (!AssignStmt.LhsIsToGhost(lhs)) {
+            Error("compiling an assign-such-that statement with a non-ghost left-hand side is currently not supported (line {0})", stmt.Tok.line);
+            break;  // no need to say more
+          }
+        }
+
       } else if (stmt is VarDecl) {
         TrVarDecl((VarDecl)stmt, true, indent);
 
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 195495aa..a1ff0ffb 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -725,6 +725,7 @@ UpdateStmt<out Statement/*!*/ s>
      Expression lhs0;
      IToken x;
      Attributes attrs = null;
+     IToken suchThatAssume = null;
      Expression suchThat = null;
   .)
   Lhs<out e>                       (. x = e.tok; .)
@@ -738,13 +739,15 @@ UpdateStmt<out Statement/*!*/ s>
       { "," Rhs<out r, lhs0>       (. rhss.Add(r); .)
       }
     | ":|"                         (. x = t; .)
+      [ "assume"                   (. suchThatAssume = t; .)
+      ]
       Expression<out suchThat>
     )
     ";"
   | ":"                            (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
   )
   (. if (suchThat != null) {
-       s = new AssignSuchThatStmt(x, lhss, suchThat);
+       s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
      } else {
        s = new UpdateStmt(x, lhss, rhss);
      }
@@ -807,6 +810,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
      AssignmentRhs r;  IdentifierExpr lhs0;
      List<VarDecl> lhss = new List<VarDecl>();
      List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+     IToken suchThatAssume = null;
      Expression suchThat = null;
   .)
   [ "ghost"                                 (. isGhost = true;  x = t; .)
@@ -824,6 +828,8 @@ VarDeclStatement<.out Statement/*!*/ s.>
     { "," Rhs<out r, lhs0>         (. rhss.Add(r); .)
     }
   | ":|"                           (. assignTok = t; .)
+    [ "assume"                     (. suchThatAssume = t; .)
+    ]
     Expression<out suchThat>
   ]
   ";"
@@ -833,7 +839,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
        foreach (var lhs in lhss) {
          ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
        }
-       update = new AssignSuchThatStmt(assignTok, ies, suchThat);
+       update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
      } else if (rhss.Count == 0) {
        update = null;
      } else {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 95110629..f8b78692 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1703,14 +1703,22 @@ namespace Microsoft.Dafny {
 
   public class AssignSuchThatStmt : ConcreteUpdateStatement
   {
-    public readonly AssumeStmt Assume;
-    public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr)
+    public readonly Expression Expr;
+    public readonly IToken AssumeToken;
+    /// <summary>
+    /// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists.
+    /// If "assumeToken" is non-null, then it should denote the "assume" keyword used in the statement.
+    /// </summary>
+    public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr, IToken assumeToken)
       : base(tok, lhss) {
       Contract.Requires(tok != null);
       Contract.Requires(cce.NonNullElements(lhss));
       Contract.Requires(lhss.Count != 0);
       Contract.Requires(expr != null);
-      Assume = new AssumeStmt(tok, expr);
+      Expr = expr;
+      if (assumeToken != null) {
+        AssumeToken = assumeToken;
+      }
     }
   }
 
@@ -1771,6 +1779,24 @@ namespace Microsoft.Dafny {
         }
       }
     }
+
+    /// <summary>
+    /// This method assumes "lhs" has been successfully resolved.
+    /// </summary>
+    public static bool LhsIsToGhost(Expression lhs) {
+      Contract.Requires(lhs != null);
+      lhs = lhs.Resolved;
+      if (lhs is IdentifierExpr) {
+        var x = (IdentifierExpr)lhs;
+        return x.Var.IsGhost;
+      } else if (lhs is FieldSelectExpr) {
+        var x = (FieldSelectExpr)lhs;
+        return x.Field.IsGhost;
+      } else {
+        // LHS denotes an array element, which is always non-ghost
+        return false;
+      }
+    }
   }
 
   public class VarDecl : Statement, IVariable {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 52bbc90c..068aa2f6 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1056,11 +1056,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s = bs; 
 			break;
 		}
-		case 65: {
+		case 66: {
 			AssertStmt(out s);
 			break;
 		}
-		case 66: {
+		case 54: {
 			AssumeStmt(out s);
 			break;
 		}
@@ -1076,15 +1076,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);
 			break;
 		}
-		case 58: {
+		case 59: {
 			IfStmt(out s);
 			break;
 		}
-		case 62: {
+		case 63: {
 			WhileStmt(out s);
 			break;
 		}
-		case 64: {
+		case 65: {
 			MatchStmt(out s);
 			break;
 		}
@@ -1136,7 +1136,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
 		Expression/*!*/ e = null; Attributes attrs = null;
 		
-		Expect(65);
+		Expect(66);
 		x = t; s = null;
 		while (IsAttribute()) {
 			Attribute(ref attrs);
@@ -1157,7 +1157,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void AssumeStmt(out Statement/*!*/ s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 
-		Expect(66);
+		Expect(54);
 		x = t; 
 		Expression(out e);
 		Expect(18);
@@ -1188,6 +1188,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression lhs0;
 		IToken x;
 		Attributes attrs = null;
+		IToken suchThatAssume = null;
 		Expression suchThat = null;
 		
 		Lhs(out e);
@@ -1218,6 +1219,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else if (la.kind == 53) {
 				Get();
 				x = t; 
+				if (la.kind == 54) {
+					Get();
+					suchThatAssume = t; 
+				}
 				Expression(out suchThat);
 			} else SynErr(145);
 			Expect(18);
@@ -1226,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 
 		} else SynErr(146);
 		if (suchThat != null) {
-		 s = new AssignSuchThatStmt(x, lhss, suchThat);
+		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
 		} else {
 		 s = new UpdateStmt(x, lhss, rhss);
 		}
@@ -1239,6 +1244,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		AssignmentRhs r;  IdentifierExpr lhs0;
 		List<VarDecl> lhss = new List<VarDecl>();
 		List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+		IToken suchThatAssume = null;
 		Expression suchThat = null;
 		
 		if (la.kind == 8) {
@@ -1271,6 +1277,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {
 				Get();
 				assignTok = t; 
+				if (la.kind == 54) {
+					Get();
+					suchThatAssume = t; 
+				}
 				Expression(out suchThat);
 			}
 		}
@@ -1281,7 +1291,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		 foreach (var lhs in lhss) {
 		   ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
 		 }
-		 update = new AssignSuchThatStmt(assignTok, ies, suchThat);
+		 update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
 		} else if (rhss.Count == 0) {
 		 update = null;
 		} else {
@@ -1306,7 +1316,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;
 		ifStmt = dummyStmt;  // to please the compiler
 		
-		Expect(58);
+		Expect(59);
 		x = t; 
 		if (la.kind == 27 || la.kind == 33) {
 			if (la.kind == 33) {
@@ -1316,9 +1326,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				guardOmitted = true; 
 			}
 			BlockStmt(out thn, out bodyStart, out bodyEnd);
-			if (la.kind == 59) {
+			if (la.kind == 60) {
 				Get();
-				if (la.kind == 58) {
+				if (la.kind == 59) {
 					IfStmt(out s);
 					els = s; 
 				} else if (la.kind == 6) {
@@ -1351,7 +1361,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;
 		stmt = dummyStmt;  // to please the compiler
 		
-		Expect(62);
+		Expect(63);
 		x = t; 
 		if (la.kind == 27 || la.kind == 33) {
 			if (la.kind == 33) {
@@ -1395,11 +1405,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);
 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;
 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 
-		Expect(64);
+		Expect(65);
 		x = t; 
 		Expression(out e);
 		Expect(6);
-		while (la.kind == 60) {
+		while (la.kind == 61) {
 			CaseStatement(out c);
 			cases.Add(c); 
 		}
@@ -1476,16 +1486,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler
 		Attributes attrs = null;
 		
-		if (la.kind == 54) {
+		if (la.kind == 55) {
 			Get();
 			newToken = t; 
 			TypeAndToken(out x, out ty);
-			if (la.kind == 33 || la.kind == 43 || la.kind == 55) {
-				if (la.kind == 55) {
+			if (la.kind == 33 || la.kind == 43 || la.kind == 56) {
+				if (la.kind == 56) {
 					Get();
 					ee = new List<Expression>(); 
 					Expressions(ee);
-					Expect(56);
+					Expect(57);
 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
 					
 				} else if (la.kind == 43) {
@@ -1527,7 +1537,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);
 			}
 			
-		} else if (la.kind == 57) {
+		} else if (la.kind == 58) {
 			Get();
 			x = t; 
 			Expression(out e);
@@ -1550,13 +1560,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		if (la.kind == 1) {
 			DottedIdentifiersAndFunction(out e);
-			while (la.kind == 43 || la.kind == 55) {
+			while (la.kind == 43 || la.kind == 56) {
 				Suffix(ref e);
 			}
 		} else if (StartOf(15)) {
 			ConstAtomExpression(out e);
 			Suffix(ref e);
-			while (la.kind == 43 || la.kind == 55) {
+			while (la.kind == 43 || la.kind == 56) {
 				Suffix(ref e);
 			}
 		} else SynErr(152);
@@ -1593,11 +1603,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;
 		
 		Expect(6);
-		while (la.kind == 60) {
+		while (la.kind == 61) {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(61);
+			Expect(62);
 			body = new List<Statement>(); 
 			while (StartOf(10)) {
 				Stmt(body);
@@ -1615,7 +1625,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;
 		
 		while (StartOf(16)) {
-			if (la.kind == 29 || la.kind == 63) {
+			if (la.kind == 29 || la.kind == 64) {
 				Invariant(out invariant);
 				while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}
 				Expect(18);
@@ -1653,12 +1663,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 
 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {
 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 
-		while (!(la.kind == 0 || la.kind == 29 || la.kind == 63)) {SynErr(159); Get();}
+		while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();}
 		if (la.kind == 29) {
 			Get();
 			isFree = true; 
 		}
-		Expect(63);
+		Expect(64);
 		while (IsAttribute()) {
 			Attribute(ref attrs);
 		}
@@ -1673,7 +1683,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;
 		List<Statement/*!*/> body = new List<Statement/*!*/>();
 		
-		Expect(60);
+		Expect(61);
 		x = t; 
 		Ident(out id);
 		if (la.kind == 33) {
@@ -1687,7 +1697,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			Expect(34);
 		}
-		Expect(61);
+		Expect(62);
 		while (StartOf(10)) {
 			Stmt(body);
 		}
@@ -2032,18 +2042,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 
 			break;
 		}
-		case 19: case 38: case 58: case 64: case 65: case 66: case 101: case 102: case 103: case 104: {
+		case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {
 			EndlessExpression(out e);
 			break;
 		}
 		case 1: {
 			DottedIdentifiersAndFunction(out e);
-			while (la.kind == 43 || la.kind == 55) {
+			while (la.kind == 43 || la.kind == 56) {
 				Suffix(ref e);
 			}
 			break;
 		}
-		case 6: case 55: {
+		case 6: case 56: {
 			DisplayExpr(out e);
 			break;
 		}
@@ -2057,7 +2067,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}
 		case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
 			ConstAtomExpression(out e);
-			while (la.kind == 43 || la.kind == 55) {
+			while (la.kind == 43 || la.kind == 56) {
 				Suffix(ref e);
 			}
 			break;
@@ -2096,18 +2106,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> letVars;  List<Expression> letRHSs;
 		
 		switch (la.kind) {
-		case 58: {
+		case 59: {
 			Get();
 			x = t; 
 			Expression(out e);
 			Expect(99);
 			Expression(out e0);
-			Expect(59);
+			Expect(60);
 			Expression(out e1);
 			e = new ITEExpr(x, e, e0, e1); 
 			break;
 		}
-		case 64: {
+		case 65: {
 			MatchExpression(out e);
 			break;
 		}
@@ -2119,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ComprehensionExpr(out e);
 			break;
 		}
-		case 65: {
+		case 66: {
 			Get();
 			x = t; 
 			Expression(out e0);
@@ -2128,7 +2138,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 
 			break;
 		}
-		case 66: {
+		case 54: {
 			Get();
 			x = t; 
 			Expression(out e0);
@@ -2208,7 +2218,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 
 			}
 			if (!func) { e = new ExprDotName(id, e, id.val); } 
-		} else if (la.kind == 55) {
+		} else if (la.kind == 56) {
 			Get();
 			x = t; 
 			if (StartOf(9)) {
@@ -2225,7 +2235,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();
 					Expression(out ee);
 					e1 = ee; 
-				} else if (la.kind == 20 || la.kind == 56) {
+				} else if (la.kind == 20 || la.kind == 57) {
 					while (la.kind == 20) {
 						Get();
 						Expression(out ee);
@@ -2267,7 +2277,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }
 			}
 			
-			Expect(56);
+			Expect(57);
 		} else SynErr(173);
 	}
 
@@ -2284,14 +2294,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			e = new SetDisplayExpr(x, elements);
 			Expect(7);
-		} else if (la.kind == 55) {
+		} else if (la.kind == 56) {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(9)) {
 				Expressions(elements);
 			}
 			e = new SeqDisplayExpr(x, elements); 
-			Expect(56);
+			Expect(57);
 		} else SynErr(174);
 	}
 
@@ -2329,14 +2339,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		Expect(41);
 		x = t; 
-		if (la.kind == 55) {
+		if (la.kind == 56) {
 			Get();
 			elements = new List<ExpressionPair/*!*/>(); 
 			if (StartOf(9)) {
 				MapLiteralExpressions(out elements);
 			}
 			e = new MapDisplayExpr(x, elements);
-			Expect(56);
+			Expect(57);
 		} else if (la.kind == 1) {
 			BoundVar/*!*/ bv;
 			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2472,10 +2482,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;
 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
 		
-		Expect(64);
+		Expect(65);
 		x = t; 
 		Expression(out e);
-		while (la.kind == 60) {
+		while (la.kind == 61) {
 			CaseExpression(out c);
 			cases.Add(c); 
 		}
@@ -2542,7 +2552,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;
 		Expression/*!*/ body;
 		
-		Expect(60);
+		Expect(61);
 		x = t; 
 		Ident(out id);
 		if (la.kind == 33) {
@@ -2556,7 +2566,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			Expect(34);
 		}
-		Expect(61);
+		Expect(62);
 		Expression(out body);
 		c = new MatchCaseExpr(x, id.val, arguments, body); 
 	}
@@ -2610,7 +2620,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	static readonly bool[,]/*!*/ set = {
-		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
@@ -2619,18 +2629,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
-		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, x,T,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
 		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
-		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
-		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
+		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
 
 	};
 } // end Parser
@@ -2709,19 +2719,19 @@ public class Errors {
 			case 51: s = "\"return\" expected"; break;
 			case 52: s = "\":=\" expected"; break;
 			case 53: s = "\":|\" expected"; break;
-			case 54: s = "\"new\" expected"; break;
-			case 55: s = "\"[\" expected"; break;
-			case 56: s = "\"]\" expected"; break;
-			case 57: s = "\"choose\" expected"; break;
-			case 58: s = "\"if\" expected"; break;
-			case 59: s = "\"else\" expected"; break;
-			case 60: s = "\"case\" expected"; break;
-			case 61: s = "\"=>\" expected"; break;
-			case 62: s = "\"while\" expected"; break;
-			case 63: s = "\"invariant\" expected"; break;
-			case 64: s = "\"match\" expected"; break;
-			case 65: s = "\"assert\" expected"; break;
-			case 66: s = "\"assume\" expected"; break;
+			case 54: s = "\"assume\" expected"; break;
+			case 55: s = "\"new\" expected"; break;
+			case 56: s = "\"[\" expected"; break;
+			case 57: s = "\"]\" expected"; break;
+			case 58: s = "\"choose\" expected"; break;
+			case 59: s = "\"if\" expected"; break;
+			case 60: s = "\"else\" expected"; break;
+			case 61: s = "\"case\" expected"; break;
+			case 62: s = "\"=>\" expected"; break;
+			case 63: s = "\"while\" expected"; break;
+			case 64: s = "\"invariant\" expected"; break;
+			case 65: s = "\"match\" expected"; break;
+			case 66: s = "\"assert\" expected"; break;
 			case 67: s = "\"print\" expected"; break;
 			case 68: s = "\"parallel\" expected"; break;
 			case 69: s = "\"<==>\" expected"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index e58a39de..fb46ba4b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -661,7 +661,10 @@ namespace Microsoft.Dafny {
       } else if (s is AssignSuchThatStmt) {
         var update = (AssignSuchThatStmt)s;
         wr.Write(" :| ");
-        PrintExpression(update.Assume.Expr);
+        if (update.AssumeToken != null) {
+          wr.Write("assume ");
+        }
+        PrintExpression(update.Expr);
       } else {
         Contract.Assert(s == null);  // otherwise, unknown type
       }
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index ba3cae19..51b22443 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -493,7 +493,7 @@ namespace Microsoft.Dafny {
 
       } else if (stmt is AssignSuchThatStmt) {
         var s = (AssignSuchThatStmt)stmt;
-        r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Assume.Expr));
+        r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken));
 
       } else if (stmt is UpdateStmt) {
         var s = (UpdateStmt)stmt;
@@ -914,7 +914,7 @@ namespace Microsoft.Dafny {
                   doMerge = true;
                 } else if (cOld.Update is AssignSuchThatStmt) {
                   doMerge = true;
-                  addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Assume.Expr);
+                  addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);
                 } else {
                   var updateOld = (UpdateStmt)cOld.Update;  // if cast fails, there are more ConcreteUpdateStatement subclasses than expected
                   if (updateOld.Rhss.Count == 1 && updateOld.Rhss[0] is HavocRhs) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6cf215d6..3ff0c12b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1845,7 +1845,9 @@ namespace Microsoft.Dafny {
       int prevErrorCount = ErrorCount;
       // First, resolve all LHS's and expression-looking RHS's.
       SeqSelectExpr arrayRangeLhs = null;
+      var update = s as UpdateStmt;
       foreach (var lhs in s.Lhss) {
+        var ec = ErrorCount;
         if (lhs is SeqSelectExpr) {
           var sse = (SeqSelectExpr)lhs;
           ResolveSeqSelectExpr(sse, true, true);
@@ -1855,14 +1857,24 @@ namespace Microsoft.Dafny {
         } else {
           ResolveExpression(lhs, true);
         }
+        if (update == null && ec == ErrorCount && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {
+          Error(lhs, "cannot assign to non-ghost variable in a ghost context");
+        }
       }
       IToken firstEffectfulRhs = null;
       CallRhs callRhs = null;
-      var update = s as UpdateStmt;
       // Resolve RHSs
       if (update == null) {
         var suchThat = (AssignSuchThatStmt)s;  // this is the other possible subclass
-        s.ResolvedStatements.Add(suchThat.Assume);
+        ResolveExpression(suchThat.Expr, true);
+        if (suchThat.AssumeToken == null) {
+          // to ease in the verification, only allow local variables as LHSs
+          foreach (var lhs in s.Lhss) {
+            if (!(lhs.Resolved is IdentifierExpr)) {
+              Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");
+            }
+          }
+        }
       } else {
         foreach (var rhs in update.Rhss) {
           bool isEffectful;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 2388716b..d35fc22f 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -520,16 +520,16 @@ public class Scanner {
 			case "label": t.kind = 49; break;
 			case "break": t.kind = 50; break;
 			case "return": t.kind = 51; break;
-			case "new": t.kind = 54; break;
-			case "choose": t.kind = 57; break;
-			case "if": t.kind = 58; break;
-			case "else": t.kind = 59; break;
-			case "case": t.kind = 60; break;
-			case "while": t.kind = 62; break;
-			case "invariant": t.kind = 63; break;
-			case "match": t.kind = 64; break;
-			case "assert": t.kind = 65; break;
-			case "assume": t.kind = 66; break;
+			case "assume": t.kind = 54; break;
+			case "new": t.kind = 55; break;
+			case "choose": t.kind = 58; break;
+			case "if": t.kind = 59; break;
+			case "else": t.kind = 60; break;
+			case "case": t.kind = 61; break;
+			case "while": t.kind = 63; break;
+			case "invariant": t.kind = 64; break;
+			case "match": t.kind = 65; break;
+			case "assert": t.kind = 66; break;
 			case "print": t.kind = 67; break;
 			case "parallel": t.kind = 68; break;
 			case "in": t.kind = 82; break;
@@ -666,11 +666,11 @@ public class Scanner {
 			case 27:
 				{t.kind = 53; break;}
 			case 28:
-				{t.kind = 55; break;}
-			case 29:
 				{t.kind = 56; break;}
+			case 29:
+				{t.kind = 57; break;}
 			case 30:
-				{t.kind = 61; break;}
+				{t.kind = 62; break;}
 			case 31:
 				if (ch == '>') {AddCh(); goto case 32;}
 				else {goto case 0;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2325734f..a98b49fd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3414,7 +3414,11 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignSuchThatStmt) {
         var s = (AssignSuchThatStmt)stmt;
         AddComment(builder, s, "assign-such-that statement");
-        // treat like a parallel havoc, followed by an assume
+        // Essentially, treat like an assert, a parallel havoc, and an assume.  However, we also need to check
+        // the well-formedness of the expression, which is easiest to do after the havoc.  So, we do the havoc
+        // first, then the well-formedness check, then the assert (unless the whole statement is an assume), and
+        // finally the assume.
+
         // Here comes the havoc part
         var lhss = new List<Expression>();
         var havocRhss = new List<AssignmentRhs>();
@@ -3426,8 +3430,36 @@ namespace Microsoft.Dafny {
         List<Bpl.IdentifierExpr> bLhss;
         ProcessLhss(lhss, false, builder, locals, etran, out lhsBuilder, out bLhss);
         ProcessRhss(lhsBuilder, bLhss, lhss, havocRhss, builder, locals, etran);
+        // Here comes the well-formedness check
+        TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
+        // Here comes the assert part
+        if (s.AssumeToken == null) {
+          var substMap = new Dictionary<IVariable, Expression>();
+          var bvars = new List<BoundVar>();
+          foreach (var lhs in s.Lhss) {
+            var l = lhs.Resolved;
+            if (l is IdentifierExpr) {
+              var x = (IdentifierExpr)l;
+              BoundVar bv;
+              IdentifierExpr ie;
+              CloneVariableAsBoundVar(x.tok, x.Var, "$as#" + x.Name, out bv, out ie);
+              bvars.Add(bv);
+              substMap.Add(x.Var, ie);
+            } else {
+              // other forms of LHSs have been ruled out by the resolver (it would be possible to
+              // handle them, but it would involve heap-update expressions--the translation would take
+              // effort, and it's not certain that the existential would be successful in verification).
+              Contract.Assume(false);  // unexpected case
+            }
+          }
+          var bvs = new VariableSeq();
+          var typeAntecedent = etran.TrBoundVariables(bvars, bvs);
+          var substE = etran.TrExpr(Substitute(s.Expr, null, substMap));
+          var ex = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, substE));
+          builder.Add(Assert(s.Tok, ex, "cannot establish the existence of LHS values that satisfy the such-that predicate"));
+        }
         // End by doing the assume
-        TrStmt(s.Assume, builder, locals, etran);
+        builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));
         builder.Add(CaptureState(s.Tok));  // just do one capture state--here, at the very end (that is, don't do one before the assume)
 
       } else if (stmt is UpdateStmt) {
-- 
cgit v1.2.3