4 files changed, 34 insertions, 9 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 370e3c38..e7fda470 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,10 +91,11 @@ TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a sub
 TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
 TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(105,15): Error: ghost variables are allowed only in specification contexts
+TypeTests.dfy(115,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(116,7): Error: cannot assign to non-ghost variable in a ghost context
 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-36 resolution/type errors detected in TypeTests.dfy
+37 resolution/type errors detected in TypeTests.dfy
 
 -------------------- NatTypes.dfy --------------------
 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
@@ -556,7 +557,9 @@ ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)
 ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool (instead got int)
 ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-62 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(434,7): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(440,12): Error: ghost variables are allowed only in specification contexts
+64 resolution/type errors detected in ResolutionErrors.dfy
 
 -------------------- ParseErrors.dfy --------------------
 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 7c919b2a..d5fecdf8 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -423,3 +423,27 @@ class Lamb {
   method Jesus() { }
   method Gwen() { }
 }
+
+// ------------------- assign-such-that and ghosts ------------------------------
+
+method AssignSuchThatFromGhost()
+{
+  var x: int;
+  ghost var g: int;
+
+  x := g;  // error: ghost cannot flow into non-ghost
+  
+  x := *;
+  assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,
+                  // the compiler will complain)
+
+  x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well
+
+  x :| assume x == g;  // this is cool, since it's an assume (but, of course, the
+                       // compiler will complain)
+
+  x :| x == 5;
+  g :| g <= g;
+  g :| assume g < g;  // the compiler will complain here, despite the LHS being
+                      // ghost -- and rightly so, since an assume is used
+}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 7b409a67..43ee1d8e 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -530,7 +530,7 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
 
 method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)
 {
-  var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'
+  ghost var k :| assume 0 <= k < a - b;  // this acts like an 'assume 0 < a - b;'
   assert b < a;
   k :| k == old(2*k);  // note, the 'old' has no effect on local variables like k
   assert k == 0;
@@ -571,7 +571,7 @@ method AssignSuchThat4()
 
 method AssignSuchThat5()
 {
-  var n := new Node;
+  ghost var n := new Node;
   n :| fresh(n);  // fine
   assert false;  // error
 }
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 2dea7a52..42457918 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -101,10 +101,8 @@ method M()
   ghost var k: int, l: int;
   var m: int;
 
-  // These three statements are allowed by the resolver, but the compiler will complain
-  // if it ever gets them.
   k :| k < 10;
-  k, m :| 0 <= k < m;
+  k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost
   m :| m < 10;
 
   // Because of the ghost guard, these 'if' statements are ghost contexts, so only