Added by Sepideh Asadi about 5 years ago. Updated about 5 years ago.
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
| ex13-change-orig.c (348 Bytes) ex13-change-orig.c | Sepideh Asadi, 26/09/2019 13:47 | ||
| query_default-1.smt2 (10.5 KB) query_default-1.smt2 | Sepideh Asadi, 26/09/2019 13:47 |
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!