Even we pass makeAssume parameter as false to the DoRelax function computation of check command
seems working like violating the firs assertion fail and assuming the rest as dischareged.
Id #10710 | Release:
| Updated: Feb 2, 2013 at 4:40 AM by kuruis | Created: Dec 30, 2012 at 1:59 PM by kuruis
TSO modelling code attached includes return statements in its read and readTID functions.
While inlining read and readTID functions which include return statement , QED runtime throws index out o...
Id #10709 | Release:
| Updated: Feb 2, 2013 at 4:40 AM by kuruis | Created: Dec 30, 2012 at 1:39 PM by kuruis