From 7ee036cae0cc6a2d48786f18908f26de37136236 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 1 Apr 2013 14:28:37 -0700
Subject: Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference
 phase, where more type information is known Refactored
 ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
 Fixed numerous places where some recursive checks did not reach.

---
 Test/VSComp2010/Problem4-Queens.dfy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/VSComp2010')

diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index 2f21b7a1..2d4111db 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -34,7 +34,7 @@ method Search(N: int) returns (success: bool, board: seq<int>)
               |board| == N &&
               (forall p :: 0 <= p && p < N ==> IsConsistent(board, p));
   ensures !success ==>
-              (forall B ::
+              (forall B: seq<int> ::
                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N)
                   ==>
                   (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
@@ -66,7 +66,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
               |newBoard| == N &&
               (forall p :: 0 <= p && p < N ==> IsConsistent(newBoard, p));
   ensures !success ==>
-              (forall B ::
+              (forall B: seq<int> ::
                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
                   boardSoFar <= B
                   ==>
@@ -84,7 +84,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
     var n := 0;
     while (n < N)
       invariant n <= N;
-      invariant (forall B ::
+      invariant (forall B: seq<int> ::
                   // For any board 'B' with 'N' queens, each placed in an existing row
                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
                   // ... where 'B' is an extension of 'boardSoFar'
@@ -122,7 +122,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
       } else {
         // Since 'n' is not a consistent placement for a queen in column 'pos', there is also
         // no extension of 'candidateBoard' that would make the entire board consistent.
-        assert (forall B ::
+        assert (forall B: seq<int> ::
                   |B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
                   candidateBoard <= B
                   ==>
-- 
cgit v1.2.3