refutation unsoundness issue on a QF_AFP instance

[zhendongsu]

Commit: 938a89e
OS: Ubuntu 22.04

[539] % z3release small.smt2 
unsat
sat
[540] % cat small.smt2 
(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (bvslt ((_ sign_extend 32) (ite (fp.eq (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) (bvnand (_ bv1 64) (concat (select d (_ bv0 32)) (select d (_ bv1 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)))))) (_ bv0 32) (_ bv1 32))) (_ bv0 64))))
(check-sat)

(reset)

(define-fun d () (Array (_ BitVec 32) (_ BitVec 8)) (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #x01) #x00000001 #x00))
(assert (not (bvslt ((_ sign_extend 32) (ite (fp.eq (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) (bvnand (_ bv1 64) (concat (select d (_ bv0 32)) (select d (_ bv1 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)) (select d (_ bv0 32)))))) (_ bv0 32) (_ bv1 32))) (_ bv0 64))))
(check-sat)

[zhendongsu]

Another (incremental) instance:

[514] % z3release small.smt2 
sat
unsat
sat
sat
[515] % cat small.smt2 
(declare-const s (_ BitVec 31))
(assert (not (fp.lt ((_ to_fp 8 24) ((_ zero_extend 1) s)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
(check-sat)
(assert (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvadd (_ bv1 32) ((_ zero_extend 1) s)))))
(check-sat)

(reset)

(define-fun s () (_ BitVec 31) #b1111111111111111111111111111111)
(assert (not (fp.lt ((_ to_fp 8 24) ((_ zero_extend 1) s)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
(check-sat)
(assert (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvadd (_ bv1 32) ((_ zero_extend 1) s)))))
(check-sat)

[zhendongsu]

[513] % z3release small.smt2 
unsat
sat
[514] % cat small.smt2 
(declare-fun s () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvnand (_ bv1 32) (concat (select s (_ bv0 32)) (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32))))))))
(check-sat)

(reset)

(define-fun s () (Array (_ BitVec 32) (_ BitVec 8)) (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #x01) #x00000001 #x00))
(assert (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvnand (_ bv1 32) (concat (select s (_ bv0 32)) (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32))))))))
(check-sat)

[zhendongsu]

[535] % z3release small.smt2 
sat
unsat
sat
sat
[536] % cat small.smt2 
(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]

An invalid model issue:

[550] % z3release model_validate=true small.smt2 
sat
(error "line 5 column 10: an invalid model was generated")
(
  (define-fun i () (Array (_ BitVec 32) (_ BitVec 8))
    ((as const (Array (_ BitVec 32) (_ BitVec 8))) #x80))
  (define-fun f () (_ BitVec 64)
    #xc440000000000000)
)
[551] % cat small.smt2 
(set-option :smt.phase_selection 1)
(declare-fun i () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun f () (_ BitVec 64))
(assert (= (fp.add roundNearestTiesToEven (fp (_ bv1 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) roundNearestTiesToEven (concat (select i (_ bv0 32)) (_ bv0 63)))) ((_ to_fp 11 53) f)))
(check-sat)
(get-model)

[zhendongsu]

A solution unsoundness issue (with the ctx-solver-simplify tactic):

[508] % z3release small.smt2
unsat
sat
[509] % cat small.smt2
(declare-fun a () (_ BitVec 32))
(assert (fp.eq ((_ to_fp 8 24) (bvnand (_ bv24 32) a)) ((_ to_fp 8 24) a)))
(check-sat)
(check-sat-using ctx-solver-simplify)

[zhendongsu]

An invalid model issue:

[513] % z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
[514] % cat small.smt2
(set-option :rewriter.cache_all true)
(set-option :smt.threads 2)
(declare-fun i0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun f () (_ BitVec 64))
(assert (= ((_ to_fp 11 53) roundNearestTiesToEven (concat (select i0 (_ bv3 32)) (select i0 (_ bv2 32)) (select i0 (_ bv1 32)) (select i0 (_ bv0 32)))) ((_ to_fp 11 53) f)))
(check-sat)

[zhendongsu]

An invalid model issue:

[508] % z3release model_validate=true small.smt2
sat
sat
(error "line 8 column 10: an invalid model was generated")
[509] % cat small.smt2
(set-option :smt.phase_selection 0)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(assert (bvule (select a (_ bv1 32)) (_ bv1 32)))
(check-sat)
(assert (= ((_ to_fp 8 24) b) ((_ to_fp 8 24) RTP c)))
(check-sat)