From 7c950ff9a2444a4664243be1eb9fe744d1f4fc87 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 18 Apr 2015 16:04:43 -0700 Subject: changed aux attribute to ghost --- Test/og/wsq.bpl | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'Test') diff --git a/Test/og/wsq.bpl b/Test/og/wsq.bpl index 9cb6a19b..f4964258 100644 --- a/Test/og/wsq.bpl +++ b/Test/og/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 {:aux} oldH:int; - var {:aux} oldT:int; - var {:aux} oldStatusT:bool; + var {:ghost} oldH:int; + var {:ghost} oldT:int; + var {:ghost} oldStatusT:bool; oldH := H; @@ -147,8 +147,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 {:aux} oldH:int; - var {:aux} oldT:int; + var {:ghost} oldH:int; + var {:ghost} oldT:int; oldH := H; oldT := T; @@ -322,8 +322,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 {:aux} oldH:int; - var {:aux} oldT:int; + var {:ghost} oldH:int; + var {:ghost} oldT:int; oldH := H; oldT := T; -- cgit v1.2.3