Menu
▾
▴
#192 Wrong PO generated
In the attached project, the PO
evt1/inv3/INV : var3' = var1' |-> var1'
should be:
evt1/inv3/INV : var3' = var1' |-> var1
(No quote for the right member of the pair.)
This is the only PO left unproved in the project (it is in fact not provable).
Event evt2 is semantically equivalent to event evt1 but the corresponding PO is correct :
evt2/inv3/INV : var3' = var1' |-> var2'
Project with wrong PO
Logged In: YES
user_id=1041912
Originator: NO
This bug has been reproduced and I agree with your analysis.
Logged In: YES
user_id=1041912
Originator: NO
Bug fixed in CVS.
The fix will be available in the next release.