Soundness Bug with QF_NRA formula.

[KJongUk]

(declare-fun c () Real)
(declare-fun d () Real)
(assert (<= c (- 8.0)))
(assert (<= (- 0.5) d))
(assert (<= d 1.0))
(assert (<= (* d (- c)) c))
(check-sat)

when execute above formula in dreal 'dreal --precision 1e-9 --model file.smt2',
dReal returns 'delta-sat'.

delta-sat with delta = 1e-100
c : [-1.797693134862315708e+308, -1.797693134862315708e+308]
d : [-0.1666666666666666852, -0.1666666666666666852]

But I think this formula is unsat.

and according to following unsatisfiable formula, dreal returns 'delta-sat'.

(declare-fun x () Real)
(declare-fun y () Real)
(assert (<= y (- 2.0)))
(assert (> x 2.0))
(assert (<= (/ y x) y))
(check-sat)

But I also think this formula is unsat. Thank you.

Version Info:
dReal : 'dReal v4.21.06.2 (Release Build)'
OS :

Distributor ID:	Ubuntu
Description:	Ubuntu 18.04.3 LTS
Release:	18.04
Codename:	bionic

[soonhokong]

Hi,

1. delta-sat doesn't not exclude the case where the original formula is unsatisfiable. It merely indicates that the delta-perturbation of the original formula is satisfiable.

2. If you provide finite bounds on c, x, y, they will turn into UNSAT. In theory, dReal should be able to branch on any interval i if |i| > delta. However, because our implementation is using IEEE-754 doubles to represent intervals, it is possible to have a case where |i| > delta but we cannot find subintervals i1 and i2 which cover i. We have been thinking about a better way to handle this case. We will update the solver behavior in the future.