From 800885b4d7d0164803c0c2f117b78c65479283f9 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Sun, 20 Sep 2015 21:51:42 -0700
Subject: Preliminary refactoring of ghost-statement computations to after type
 checking

---
 Test/dafny0/AssumptionVariables0.dfy | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'Test/dafny0/AssumptionVariables0.dfy')

diff --git a/Test/dafny0/AssumptionVariables0.dfy b/Test/dafny0/AssumptionVariables0.dfy
index a3e23b73..b9acc522 100644
--- a/Test/dafny0/AssumptionVariables0.dfy
+++ b/Test/dafny0/AssumptionVariables0.dfy
@@ -6,7 +6,7 @@ method test0(x: int)
   ghost var {:assumption} a0 := false;  // error
   ghost var a1, {:assumption} a2 := true, false;  // error
   ghost var {:assumption} a3: bool;
-  var {:assumption} a4;  // 2 errors
+  ghost var {:assumption} a4;  // error: type must be bool
 
   a0 := a0 && (0 < x);
 
@@ -54,7 +54,7 @@ method test2()
 
       if (false)
       {
-        var {:assumption} a0: bool;  // error
+        ghost var {:assumption} a0: bool;
 
         if (false)
         {
@@ -73,3 +73,7 @@ method test2()
     }
   }
 }
+
+method test3() {
+  var {:assumption} a: bool;  // error: assumption variable must be ghost
+}
-- 
cgit v1.2.3