1 files changed, 14 insertions, 1 deletions
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);