[consolidated] new core, floats

[NikolajBjorner]

[529] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 76 147: (= (extract[31:31] (bv_wrap a)) (extract[31:31] (bv_wrap #80))) true
(sat
...
[530] % cat small.smt2
(declare-fun a () Float32)
(assert (forall ((b Float32)) (not (fp.isPositive (fp.max a b)))))
(check-sat)

[NikolajBjorner]

$ z3release tactic.default_tactic=smt sat.euf=true small.smt2 
unsat
$ z3-4.8.9 tactic.default_tactic=smt sat.euf=true small.smt2 
sat
$ cvc5 -q small.smt2
sat
$ cat small.smt2
(assert (= ((_ to_fp 5 11) roundTowardNegative (concat (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1))) ((_ to_fp 5 11) roundTowardNegative (concat (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1)))))
(check-sat)

[NikolajBjorner]

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/util/mpf.cpp
Line: 1966
m_mpz_manager.lt(o.significand, p_m3)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2 
(declare-fun p () (_ FloatingPoint 2 3))
(declare-fun fp () (_ FloatingPoint 2 3))
(assert (fp.isNegative (fp.fma roundNearestTiesToEven fp p (fp (_ bv0 1) (_ bv0 2) (_ bv0 2)))))
(check-sat)

[NikolajBjorner]

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/util/mpf.cpp
Line: 1966
m_mpz_manager.lt(o.significand, p_m3)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2 
(declare-fun p () (_ FloatingPoint 2 3))
(declare-fun fp () (_ FloatingPoint 2 3))
(assert (fp.isNegative (fp.fma roundNearestTiesToEven fp p (fp (_ bv0 1) (_ bv0 2) (_ bv0 2)))))
(check-sat)

[NikolajBjorner]

Issues with floats in the new core are most likely already latent or fixed in the main core. It is better to concentrate on exercising Fp issues for the main core until the existing bugs have been dealt with.

[merlinsun]

$ cat small.smt2 
(declare-const v (_ BitVec 7))
(declare-const x (_ FloatingPoint 2 6))
(assert (or true (fp.eq x ((_ to_fp 2 6) ((_ zero_extend 1) v)))))
(check-sat-using (then sat-preprocess qsat))
$ z3 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
failed to verify: (let ((a!1 (= p!8 (= ((_ extract 4 0) (bv_wrap x)) ((_ extract 4 0) v))))
...