smt.bv.size_reduce=true unsoundness

[nunoplopes]

Take this example:

(declare-fun %db () (_ BitVec 7))
(declare-fun blk_align_tgt ((_ BitVec 3)) (_ BitVec 6))
(declare-fun blk_size ((_ BitVec 3)) (_ BitVec 4))
(declare-fun blk_align_src ((_ BitVec 3)) (_ BitVec 6))

(assert (let ((a!3 (and (bvule (bvadd #x1 ((_ extract 3 0) %db)) (blk_size ((_ extract 6 4) %db)))
                        (not (= ((_ extract 3 3) %db) #b1))
                        (bvule #b000011 (blk_align_src ((_ extract 6 4) %db)))))
               (a!7 (bvule #b000011 (blk_align_tgt ((_ extract 6 4) %db)))))
  (and (= #x0 (blk_size #b000))
       (bvule ((_ extract 6 4) %db) #b001)
       (bvule (blk_align_src #b001) (blk_align_tgt #b001))
       (and a!3 (not a!7)))))

(check-sat-using smt)

And run with and without size_reduce:

$ z3 bug.smt2; z3 smt.bv.size_reduce=true bug.smt2
unsat
sat

[zhendongsu]

Likely related:

[534] % z3release model_validate=true small.smt2 
sat
sat
[535] % z3release smt.bv.size_reduce=true model_validate=true small.smt2 
sat
sat
(error "line 6 column 10: an invalid model was generated")
[536] % cat small.smt2 
(declare-fun p () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (not (= (_ bv0 32) ((_ zero_extend 24) (select p (_ bv0 32))))))
(check-sat)
(assert (bvule ((_ zero_extend 24) (select p (_ bv0 32))) (_ bv1 32)))
(assert (= (_ bv0 32) ((_ zero_extend 24) (select p ((_ zero_extend 24) (select p ((_ zero_extend 24) (select p (_ bv0 32)))))))))
(check-sat)

[zhendongsu]

Another related instance:

[518] % z3release model_validate=true small.smt2 
sat
unsat
[519] % z3release smt.bv.size_reduce=true model_validate=true small.smt2 
sat
sat
(error "line 4 column 10: an invalid model was generated")
[520] % 
[520] % cat small.smt2 
(declare-const a (_ BitVec 26))
(check-sat)
(assert (not (= (_ bv0 1) (bvand (bvnot (bvsub (_ bv1 1) (bvudiv (_ bv0 1) (bvnot ((_ extract 25 25) a))))) (bvcomp (_ bv0 17) ((_ zero_extend 6) ((_ extract 25 15) a)))))))
(check-sat)

[zhendongsu]

Another (simpler) instance:

[581] % z3release small.smt2
unsat
[582] % z3release smt.bv.size_reduce=true model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
[583] % cat small.smt2
(declare-const a (_ BitVec 2))
(declare-const b (_ BitVec 2))
(push)
(assert (bvule ((_ zero_extend 1) b) (_ bv1 3)))
(assert (bvult (_ bv0 3) ((_ zero_extend 1) a)))
(assert (bvult a b))
(check-sat)

[zhendongsu]

[547] % z3release model_validate=true small.smt2 
sat
[548] % z3release smt.bv.size_reduce=true small.smt2 
unsat
[549] % cat small.smt2 
(declare-fun a () (_ BitVec 2))
(declare-fun b () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun c () (Array (_ BitVec 1) (_ BitVec 1)))
(define-fun d () Bool (= c c))
(assert (= c b))
(assert (not (bvult (_ bv1 4) ((_ zero_extend 2) a))))
(assert (= (_ bv0 4) (bvand (_ bv1 4) (bvadd (_ bv1 4) ((_ zero_extend 2) a)))))
(check-sat)