bug fix in the type checking of calls to atomic procedures

1 files changed, 7 insertions, 7 deletions

diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 39dad919..0a2227b6 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,9 +89,9 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
 ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
 {
    var t: int;
-   var {:ghost} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
-   var {:ghost} {:layer 3} oldStatusT:bool;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
+   var {:layer 3} oldStatusT:bool;
    
    call oldH, oldT := GhostRead();
    yield;
@@ -142,8 +142,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
    call oldH, oldT := GhostRead();
    yield;
@@ -304,8 +304,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
 {
    var h, t: int;
    var chk: bool;
-   var {:ghost} {:layer 3} oldH:int;
-   var {:ghost} {:layer 3} oldT:int;
+   var {:layer 3} oldH:int;
+   var {:layer 3} oldT:int;
 
    call oldH, oldT := GhostRead();
    yield;