For this formula, z3 gives an incorrect sat, while the model validator cannot detect.
[503] % cvc4 -q small.smt2
unsat
[504] % z3release model_validate=true small.smt2
sat
[505] % cat small.smt2
(assert (forall ((a Float32)) (not (fp.isNegative (fp.min a (_ +zero 8 24))))))
(check-sat)
[506] %
Commit: 621e992
For this formula, z3 gives an incorrect sat, while the model validator cannot detect.
Commit: 621e992