Z3 reports sat for an unsat formula.
Input:
(set-logic ALL)
(declare-const F Int)
(assert
(and
(< F 1)
(>
(let ((f ((_ to_fp 8 24) RTN (to_real F))))
(ite
(fp.isInfinite f)
0
(to_int
(fp.to_real
(fp.roundToIntegral RTN f)))))
0)))
(check-sat)Output:
$ z3 test.smt2 model_validate=true
sat
(error "line 18 column 10: an invalid model was generated")
$ cvc5 test.smt2
unsat
The formula is unsatisfiable.
Because F is an integer and F < 1, we have F <= 0. Converting it to Float32 with RTN therefore produces either -oo or a finite non-positive float.
In the former case the ite returns 0; in the latter case, fp.roundToIntegral RTN, fp.to_real, and to_int cannot make the value positive. Thus the asserted expression cannot be greater than 0.
Without model validation, adding (get-model) produces the following model:
sat
(
(define-fun F () Int
0)
(define-fun /0 ((x!0 Real) (x!1 Real)) Real
(ite (and (= x!0 1.0) (= x!1 17592186044416.0)) (/ 1.0 17592186044416.0)
(/ 1.0 85070591730234615865843651857942052864.0)))
)With a debug build the same behavior takes noticeably longer to trigger, but the outcome is identical. cvc5 returns unsat on this input. On release builds, 4.16.0 answers unknown, while 5.0.0 answers sat.
Commit: 1c89937
Z3 reports
satfor anunsatformula.Input:
Output:
The formula is unsatisfiable.
Because
Fis an integer andF < 1, we haveF <= 0. Converting it to Float32 withRTNtherefore produces either-ooor a finite non-positive float.In the former case the
itereturns0; in the latter case,fp.roundToIntegral RTN,fp.to_real, andto_intcannot make the value positive. Thus the asserted expression cannot be greater than0.Without model validation, adding
(get-model)produces the following model:With a debug build the same behavior takes noticeably longer to trigger, but the outcome is identical. cvc5 returns
unsaton this input. On release builds, 4.16.0 answersunknown, while 5.0.0 answerssat.Commit: 1c89937