Fuzz bugs for floats - unsoundness / Invalid model issue on default mode

[depted]

Greetings,
For this instance, an invalid bug occurred.
We tried to reduce the size of this instance with ddSMT. however, it failed. Hope to understand that reducing the complexity of this instance is hard.

$ ./z3 ./raw.smt2 model_validate=true
sat
(error "line 17 column 10: an invalid model was generated")

$ cat ./raw.smt2
(declare-fun v_currentRoundingMode_16 () RoundingMode)
(declare-fun v_SqrtR_~xn~0_7 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~xnp1~0_5 () (_ FloatingPoint 11 53))
(declare-fun v_~_EPS~0_6 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~residu~0_4 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~linf~0_4 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~lsup~0_4 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~cond~0_6 () (_ BitVec 32))
(declare-fun madebysaiyan_0 () (_ FloatingPoint 5 26))
(assert (= v_SqrtR_~lsup~0_4 (fp.mul v_currentRoundingMode_16 v_~_EPS~0_6 (fp.add v_currentRoundingMode_16 v_SqrtR_~xn~0_7 v_SqrtR_~xnp1~0_5))))
(assert (let ((a!1 (fp.mul v_currentRoundingMode_16 (fp.max (fp #b1 #b10000000001 #x0000000000000) ((_ to_fp 11 53) roundNearestTiesToEven (fp.rem (fp #b0 #b10000 #b0000000000000000000000000) madebysaiyan_0))) v_~_EPS~0_6))) (= (fp.mul v_currentRoundingMode_16 a!1 (fp.add v_currentRoundingMode_16 v_SqrtR_~xn~0_7 v_SqrtR_~xnp1~0_5)) v_SqrtR_~residu~0_4)))
(assert (= ((_ to_fp 11 53) v_currentRoundingMode_16 1.0) v_SqrtR_~xn~0_7))
(assert (= v_SqrtR_~linf~0_4 (fp.neg v_SqrtR_~lsup~0_4)))
(assert (= v_SqrtR_~cond~0_6 (_ bv0 32)))
(assert (= v_SqrtR_~xnp1~0_5 v_SqrtR_~xn~0_7))
(assert (not (= v_SqrtR_~cond~0_6 (ite (or (fp.lt v_SqrtR_~residu~0_4 v_SqrtR_~linf~0_4) (fp.gt v_SqrtR_~residu~0_4 v_SqrtR_~lsup~0_4)) (_ bv1 32) (_ bv0 32)))))
(check-sat)

commit: 8be43ca

[depted]

We succeeded in delta-debugging about another instance. It is way smaller than the instance that we reported before. We report this instance in hopes that it will helpful for z3 team.

(declare-const x Real)
(declare-fun v () RoundingMode)
(assert (fp.gt (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) (fp.neg ((_ to_fp 8 24) v x))))
(check-sat)

[NikolajBjorner]

Greetings,
For this instance, a refutation soundness bug occurred. Also, we checked that this instance should be "SAT". We truly hope that this instance will be helpful for the z3 team.

$ ./z3 ./small.smt2
unsat

$ cvc5 ./small.smt2
sat

$ cat ./small.smt2
(set-logic ALL)
(declare-fun c () RoundingMode)
(declare-fun m () Float32)
(assert (and (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) (fp.div c m (fp (_ bv0 1) (_ bv255 8) (_ bv0 23)))) (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) (fp.div c m ((_ to_fp 8 24) c (/ (ite (fp.geq (fp (_ bv0 1) (_ bv255 8) (_ bv0 23)) m) 1.0 0.0) 2)))))))
(check-sat)

This bug looks similar to what we reported before(#6553). Both instances caused bugs in the commit version but "unknown" in the release version(4.12.1). However, we decided to report this instance since what we reported was an invalid model bug but this one is a refutation soundness bug. Hope that this report is meaningful to the z3 team.

commit: 7c08e53

[NikolajBjorner]

Moved to consolidated: you can fuzz all you want, but these floating point bugs don't get fixed any time soon.
So, it isn't practical that they take up attention span from user bugs.
If the bugs are important to you, you can suggest fixes.

[depted]

Thanks for your kind reply. We'll take your suggestion into account.
Sincerely hope that we can contribute to fixing these bugs. :)