Bug #5011
Prop version returns SAT instead of UNSAT when using float vars
100%
Description
The issue is solved if using double instead of float
this code, it supposed to be UNSAT, but we get SAT for it:
float nondet();
float inc(float x)
{
return x + 1;
}
void
main()
{
float y = nondet();
if(y >= 0.0 && y < 1.0)
{
float z = inc(y);
assert(z < 12.4);
}
}
Its encoding is in prop, in Z3, and if you just follow the simple encoding it supposes to be UNSAT, but we get SAT. Any idea?
(declare-fun |goto_symex::\guard#1| () Bool)
(declare-fun |hifrog::?err#1| () Bool)
(declare-fun |hifrog::?fun_end#1| () Bool)
(declare-fun |hifrog::?fun_end#2| () Bool)
(declare-fun |hifrog::?fun_end#3| () Bool)
(declare-fun |hifrog::?fun_start#1| () Bool)
(declare-fun |hifrog::?fun_start#2| () Bool)
(declare-fun |hifrog::?fun_start#3| () Bool)
(declare-fun |inc::#return_value!#0| () Floatbv)
(declare-fun |inc::?return_value_tmp#1| () Floatbv)
(declare-fun |inc::x!0#1| () Floatbv)
(declare-fun |inc::x!0#2| () Floatbv)
(declare-fun |main::1::1::z!0#2| () Floatbv)
(declare-fun |main::1::y!0#2| () Floatbv)
(declare-fun |symex::nondet0| () Floatbv)
; XXX Partition: 3 (ass_in_subtree: 0) - inc (loc: 20, INL)
(assert
(and
(= |inc::x!0#2| |inc::x!0#1|)
(= |inc::?return_value_tmp#1| (+ |inc::x!0#2| 1))
(= |inc::#return_value!#0| |inc::?return_value_tmp#1|)
|hifrog::?fun_start#3|
(=> |hifrog::?fun_end#3|
(and
true
|hifrog::?fun_start#3|
)
)
)
)
; XXX Partition: 2 (ass_in_subtree: 1) - main (loc: 15, INL)
(assert
(and
(= |main::1::y!0#2| |symex::nondet0|)
(= |goto_symex::\guard#1| (not (or (not (< |main::1::y!0#2| 1)) (not (>= |main::1::y!0#2| 0)))))
(= |inc::x!0#1| |main::1::y!0#2|)
(= |main::1::1::z!0#2| |inc::#return_value!#0|)
|hifrog::?fun_start#2|
(=> |goto_symex::\guard#1| |hifrog::?fun_end#3|)
(= |hifrog::?fun_start#3|
|hifrog::?fun_start#2|
)
(not (=> |goto_symex::\guard#1| (< |main::1::1::z!0#2| 12.4)))
(= |hifrog::?err#1|
(not
(=>
(and
|hifrog::?fun_start#2|
(=> |goto_symex::\guard#1| |hifrog::?fun_end#3|)
)
(=> |goto_symex::\guard#1| (< |main::1::1::z!0#2| 12.4))
)
)
)
(=> |hifrog::?fun_end#2|
(and
true
|hifrog::?fun_start#2|
(=> |goto_symex::\guard#1| |hifrog::?fun_end#3|)
)
)
)
)
; XXX Partition: 1 (ass_in_subtree: 0) - __CPROVER_initialize (loc: 1, INL)
(assert
(and
|hifrog::?fun_start#1|
(=> |hifrog::?fun_end#1|
|hifrog::?fun_start#1|
)
)
)
; XXX Partition: 0 (ass_in_subtree: 1) - nil (loc: 0, INL)
(assert
(and
|hifrog::?fun_end#1|
|hifrog::?fun_end#2|
(= |hifrog::?fun_start#1|
true
)
(= |hifrog::?fun_start#2|
|hifrog::?fun_end#1|
)
|hifrog::?err#1|
)
)
(check-sat)
History
#1 Updated by Karine Even Mendoza almost 7 years ago
It is UNSAT in z3...(but z3 has no floatbv) so we need to check it directly into opensmt term and to play with the encoding till fixed.
#2 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from New to Feedback
- Assignee changed from Karine Even Mendoza to Antti Hyvärinen
Creates strange encoding: -340282340000000000000000000000000000000
(in LRA - but it can be something that affects other things of course)
What is this number?
(declare-fun |goto_symex::guard#1| () Bool)
(declare-fun |hifrog::?err#1| () Bool)
(declare-fun |hifrog::?fun_end#1| () Bool)
(declare-fun |hifrog::?fun_end#2| () Bool)
(declare-fun |hifrog::?fun_end#3| () Bool)
(declare-fun |hifrog::?fun_start#1| () Bool)
(declare-fun |hifrog::?fun_start#2| () Bool)
(declare-fun |hifrog::?fun_start#3| () Bool)
(declare-fun |inc::#return_value!#0| () Real)
(declare-fun |inc::?return_value_tmp#1| () Real)
(declare-fun |inc::x!0#1| () Real)
(declare-fun |inc::x!0#2| () Real)
(declare-fun |main::1::1::z!0#2| () Real)
(declare-fun |main::1::y!0#2| () Real)
(declare-fun |symex::nondet0| () Real)
; Declarations from OpenSMT2 :
(set-logic QF_LRA)
(declare-fun not (Bool ) Bool)
(declare-fun = (Bool Bool ) Bool)
(declare-fun => (Bool Bool ) Bool)
(declare-fun and (Bool Bool ) Bool)
(declare-fun or (Bool Bool ) Bool)
(declare-fun xor (Bool Bool ) Bool)
(declare-fun distinct (Bool Bool ) Bool)
(declare-fun ite (Bool Bool ) Bool)
(declare-fun = (Real Real ) Bool)
(declare-fun distinct (Real Real ) Bool)
(declare-fun ite (Bool Real Real ) Real)
(declare-fun - (Real ) Real)
(declare-fun - (Real Real ) Real)
(declare-fun + (Real Real ) Real)
(declare-fun * (Real Real ) Real)
(declare-fun / (Real Real ) Real)
(declare-fun <= (Real Real ) Bool)
(declare-fun < (Real Real ) Bool)
(declare-fun >= (Real Real ) Bool)
(declare-fun > (Real Real ) Bool)
(declare-fun |hifrog::?fun_start#3| () Bool)
(declare-fun |hifrog::?fun_end#3| () Bool)
(declare-fun |inc::x!0#2| () Real)
(declare-fun |inc::x!0#1| () Real)
(declare-fun |inc::?return_value_tmp#1| () Real)
(declare-fun |hifrog::c::unsupported_op2var!0#0| () Real)
(declare-fun |inc::#return_value!#0| () Real)
(declare-fun |hifrog::?fun_start#2| () Bool)
(declare-fun |hifrog::?fun_end#2| () Bool)
(declare-fun |hifrog::?err#1| () Bool)
(declare-fun |goto_symex::guard#1| () Bool)
(declare-fun |main::1::y!0#2| () Real)
(declare-fun |symex::nondet0| () Real)
(declare-fun |main::1::1::z!0#2| () Real)
(declare-fun |hifrog::?fun_start#1| () Bool)
(declare-fun |hifrog::?fun_end#1| () Bool)
(assert
(and
; XXX Partition: 0
(and (= |inc::x!0#2| |inc::x!0#1|) (= |inc::?return_value_tmp#1| |hifrog::c::unsupported_op2var!0#0|) (= |inc::?return_value_tmp#1| |inc::#return_value!#0|) (or |hifrog::?fun_start#3| (not |hifrog::?fun_end#3|)))
; XXX Partition: 1
(and (and (<= -340282340000000000000000000000000000000 |symex::nondet0|) (<= -340282340000000000000000000000000000000 (* |symex::nondet0| -1))) (= |main::1::y!0#2| |symex::nondet0|) (= |goto_symex::guard#1| (not (or (<= 3 |main::1::y!0#2|) (not (<= 2 |main::1::y!0#2|))))) (= |inc::x!0#1| |main::1::y!0#2|) (= |inc::#return_value!#0| |main::1::1::z!0#2|) (= (and |hifrog::?fun_start#2| |goto_symex::guard#1|) |hifrog::?fun_start#3|) (= (not (or (not (and |hifrog::?fun_start#2| (or |hifrog::?fun_end#3| (not |goto_symex::guard#1|)))) (or (not |goto_symex::guard#1|) (not (<= 62/5 |main::1::1::z!0#2|))))) |hifrog::?err#1|) (or (not |hifrog::?fun_end#2|) (and |hifrog::?fun_start#2| (or |hifrog::?fun_end#3| (not |goto_symex::guard#1|)))))
; XXX Partition: 2
(or |hifrog::?fun_start#1| (not |hifrog::?fun_end#1|))
; XXX Partition: 3
(and |hifrog::?err#1| |hifrog::?fun_start#1| (= |hifrog::?fun_end#1| |hifrog::?fun_start#2|))
))
(check-sat)
#3 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from Feedback to Closed
- Assignee changed from Antti Hyvärinen to Sepideh Asadi
- % Done changed from 0 to 100
Works now:
INTERPOLATION TIME: 0.033
; -------------------------
; STATISTICS FOR SAT SOLVER
; -------------------------
; Restarts.................: 1
; Conflicts................: 64
; Decisions................: 229
; Propagations.............: 9311
; Conflict literals........: 354
; T-Lemmata learnt.........: 0
; T-Lemmata perm learnt....: 0
; Conflicts learnt.........: 64
; T-conflicts learnt.......: 0
; Average learnts size.....: 5.3125
; Top level literals.......: 27
; Search time..............: 0 s
; TSolvers time............: 0 s
; Init clauses.............: 4070
; Variables................: 1133
; -------------------------
; STATISTICS FOR EUF SOLVER
; -------------------------
; Satisfiable calls........: 0
; Unsatisfiable calls......: 0
; egraph time..............: 0 s
; backtrack time...........: 0 s
; explain time.............: 0 s
; # eq classes at the end..: 36754104
; -------------------------
; STATISTICS FOR LOGICS
; -------------------------
; Substitutions............: 0
FUNCTION SUMMARIES (for 1 calls) WERE SUBSTITUTED SUCCESSFULLY.
VERIFICATION SUCCESSFUL
Initial unwinding bound: 4294967295
Total number of steps: 1
TOTAL TIME FOR CHECKING THIS CLAIM: 0.3
Checked Assertion:
file ex_float.c line 12 function main
assertion
FLOAT_TYPECAST(z, double, __CPROVER_rounding_mode) < 12.4
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog ex_float.c --logic prop