Merge commit 'df5c5f5'

1 files changed, 6 insertions, 2 deletions

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

+}