search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Inconsistency with CVC4 on QF_FP formula #4819

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic QF_FP)
(declare-fun fpv5 () Float32)
(assert (fp.eq (fp.mul RTP fpv5 fpv5) ((_ to_fp 8 24) RTN 0.04)))
(check-sat)

cvc4 yields sat, but z3 c27a3250174f gives unsat. cvc4 gives the following model. However, after feeding the model to z3, it still yields unsat.

(define-fun fpv5 () (_ FloatingPoint 8 24) (fp #b0 #b01111100 #b10011001100110011001101))
rainoftime commented 4 years ago

Seems to be a soundness issue in CVC4