Bug #13577
prop incorrect result
Status:
New
Priority:
Normal
Assignee:
-
Start date:
07/10/2019
Due date:
% Done:
0%
Estimated time:
Description
Benchmark: ex21-upg2.c (attached)
How to run:
./hifrog --logic prop ex21-upg2.
Error:
reported as Successful but I think a= 1 and b=1 is a CEX. Surprisingly CBMC also agrees as Successful!