Bug #13356
openBug in Hifrog LRA encoding - resulting assertion violation for a safe bench
0%
Description
Benchmark: ex13-change-orig.c (attached)
How to run:
./hifrog --logic qflra ex13-change-orig.c
Error:
LRA reports the bench as unsafe, while prop reports it as safe. The result of dump-query is SAT in OpenSMT and Z3, so the bug is in the encoding.
Files
Updated by Sepideh Asadi about 5 years ago
- Status changed from New to Resolved
This behaviour is Normal and expected in LRA, because LRA does not recognise int, all is Real number!
it is because of the following reason:
In C itself the correct behavior is a1=a2
but in LRA since in the encoding (cprover) we do optimization as
x > c --> x >= c+1
for e.g., in the following c program contains integer
int x;
if (x>0)
assert(x>=1); in C itself, and Propositional logic it is safe
in LRA it is unsafe because of different nature of LRA that does not know integer, it considers it as Real: so x= 0.5 cex is reported!