Project

General

Profile

Bug #13577

prop incorrect result

Added by Sepideh Asadi about 1 month ago.

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!

ex21-upg2.c (348 Bytes) ex21-upg2.c Sepideh Asadi, 07/10/2019 00:12

Also available in: Atom PDF