Geeting wrong delta-sat model on unsat query.

[trivedi-nitesh]

Hello everyone,

To interpret the model returned by dReal on delta-sat I tested with below encoding:

(set-logic QF_NRA)
(declare-fun f () Int)
(declare-fun p () Real)
(declare-fun z () Real)

(define-fun expr1 () Real
  (ite (= f 0)
    (+ (/ p (- 1.0 p)) z)
    0.0
  )
)

(define-fun expr2 () Real
  (ite (= f 0)
  (+ (/ p (- 1.0 p)) z)
    0.0
  )
)

(assert (<= 0 p))
(assert (<= p 1))
(assert (<= 0 z))
(assert (<= z 25))
(assert (<= 0 f))
(assert (<= f 1))
(assert (> (- expr1 expr2) 0))
(check-sat)
(exit)

In this encoding expr1 and expr2 both are same. dReal returns delta-sat on this with following model:

[debug] [20230723 11:02:17.744726] ContextImpl::CheckSat() - Found Model
f : [0, 0]
p : [0.99999999999999989, 1]
z : [8.3333333333333304, 8.3333333333333321]
expr1 : [1.7976931348623155e+308, 1.7976931348623155e+308]
ITE0 : [1.7976931348623155e+308, 1.7976931348623155e+308]
expr2 : [1.3305602063564796e+292, 1.3305602063564796e+292]
ITE1 : [1.3305602063564796e+292, 1.3305602063564796e+292]
delta-sat with delta = 0.001

I have couple of doubts:

1. Why do expr1 and expr2 evaluate to different values?
2. Why do we get delta-sat in the above case? Shouldn't it be unsat?

I'm looking forward to receiving your valuable input and insights on this matter. Thank you in advance.