[consolidated] invalid model issues on QF_ABV instances

[zhendongsu]

Commit: 9958cab
OS: Ubuntu 18.04

[507] % z3release model_validate=true small.smt2
sat
(error "line 7 column 41: an invalid model was generated")
[508] % cat small.smt2
(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun b () (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(assert (= c (bvxor b (_ bv1 1))))
(assert (not (= (_ bv0 1) (select a (_ bv0 1)))))
(assert (= b (ite (= a (store a (_ bv0 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))
(check-sat-using (then bit-blast default))

[zhendongsu]

[610] % z3release model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
[611] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(set-option :rewriter.expand_nested_stores true)
(set-option :smt.threads 2)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (= (ite (= b (store (store (store a (_ bv0 32) (_ bv1 8)) (_ bv1 32) (_ bv0 8)) (_ bv0 32) (_ bv1 8))) (_ bv1 1) (_ bv0 1)) (bvcomp (_ bv0 1) (ite (= c (store (store (store b (_ bv0 32) (_ bv0 8)) (_ bv2 32) (_ bv1 8)) (_ bv0 32) (_ bv0 8))) (_ bv1 1) (_ bv0 1)))))
(check-sat)

[zhendongsu]

[552] % z3release model_validate=true small.smt2 
sat
(error "line 6 column 61: an invalid model was generated")
[553] % cat small.smt2 
(set-option :rewriter.bit2bool false)
(declare-const x (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun e () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun t () (_ BitVec 1))
(assert (= (_ bv1 1) (bvand (bvcomp t (ite (= x (store e (_ bv0 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (distinct (_ bv1 1) (ite (= e x) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))
(check-sat-using (then ctx-solver-simplify bit-blast default))

[zhendongsu]

[536] % z3release model_validate=true small.smt2 
sat
(error "line 8 column 21: an invalid model was generated")
[537] % cat small.smt2 
(set-option :rewriter.expand_nested_stores true)
(set-option :proof true)
(set-option :smt.threads 2)
(declare-fun m () (Array (_ BitVec 32) Float32))
(declare-fun v () (Array (_ BitVec 32) Float32))
(assert (= m (store (store (store v (_ bv1 32) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))) (_ bv0 32) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))) (_ bv1 32) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
(assert (fp.gt (fp (_ bv0 1) (_ bv1 8) (_ bv0 23)) (select v (_ bv0 32))))
(check-sat-using ufbv)

[zhendongsu]

[527] % z3release model_validate=true small.smt2 
sat
(error "line 4 column 50: an invalid model was generated")
[528] % cat small.smt2 
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(assert (= a (bvnot b)))
(check-sat-using (then bit-blast aig horn default))

[wintered]

(smt.array.extensional=false)

$z3release model_validate=true smt.array.extensional=false bug.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$cat bug.smt2 
(declare-const a (Array (_ BitVec 64) (_ BitVec 64))) 
(declare-const b (_ BitVec 64)) 
(assert (distinct a (store a #x0000000000000000 #x0000000000000000))) 
(check-sat)
$

[zhendongsu]

Very similar to #5820 (comment):

[525] % z3release model_validate=true small.smt2
sat
(error "line 4 column 50: an invalid model was generated")
[526] % cat small.smt2
(declare-const a (_ BitVec 1))
(declare-const b (_ BitVec 1))
(assert (not (= a b)))
(check-sat-using (then bit-blast aig horn default))