Project

General

Profile

Bug #13356

Bug in Hifrog LRA encoding - resulting assertion violation for a safe bench

Added by Sepideh Asadi about 2 months ago. Updated about 1 month ago.

Status:
Resolved
Priority:
Normal
Assignee:
-
Start date:
26/09/2019
Due date:
% Done:

0%

Estimated time:

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.

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

History

#1 Updated by Sepideh Asadi about 1 month 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!

Also available in: Atom PDF