refutation unsoundness issue on a QF_AFP instance

[zhendongsu]

[522] % z3release small.smt2 
unsat
sat
[523] % cat small.smt2 
(declare-fun s () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (fp.leq ((_ to_fp 8 24) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32)))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))
(assert (not (fp.geq ((_ to_fp 8 24) (bvxnor (_ bv0 32) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32))))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
(check-sat)

(reset)

(define-fun s () (Array (_ BitVec 32) (_ BitVec 8)) (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #b00000000) #b00000000000000000000000000000000 #b10000000) #b00000000000000000000000000000001 #b01111111))
(assert (fp.leq ((_ to_fp 8 24) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32)))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))
(assert (not (fp.geq ((_ to_fp 8 24) (bvxnor (_ bv0 32) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32))))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
(check-sat)

[zhendongsu]

(declare-const a (_ BitVec 1))
(check-sat)
(assert (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvnand (_ bv1 32) ((_ zero_extend 31) a))))))
(check-sat)

(reset)

(define-fun a () (_ BitVec 1) #b0)
(check-sat)
(assert (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvnand (_ bv1 32) ((_ zero_extend 31) a))))))
(check-sat)

[zhendongsu]

[520] % z3release small.smt2 
unsat
sat
[521] % cat small.smt2 
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (bvsgt (_ bv0 64) (bvsmod (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32))) ((_ sign_extend 32) (ite (fp.lt (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) (bvnand (_ bv1 64) (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)))))) (_ bv1 32) (_ bv0 32))))))
(check-sat)

(reset)

(define-fun a () (Array (_ BitVec 32) (_ BitVec 8)) (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #b00000000) #b00000000000000000000000000000000 #b11111111) #b00000000000000000000000000000001 #b11111111))
(assert (bvsgt (_ bv0 64) (bvsmod (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32))) ((_ sign_extend 32) (ite (fp.lt (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) (bvnand (_ bv1 64) (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)))))) (_ bv1 32) (_ bv0 32))))))
(check-sat)

[nunoplopes]

may be related with the recent regressions #6972