Invalid model for QF_BV formula (sat.xor.solver, sat.branching.anti_exploration)

[rainoftime]

Hi, for the following formua, z3 01c12c9 gives an invalid model

(set-logic QF_BV)
(set-option :model_validate true)
(set-option :sat.xor.solver true)
(set-option :sat.branching.anti_exploration true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(push 1)
(push 1)
(pop 1)
(push 1)
(pop 1)
(declare-const v20 Bool)
(push 1)
(assert (or v9 v13 v5))
(assert (or v5 v6 v1))
(assert (or v14 (= v1 v5 v5 false v9 v10 v11 v16 v4 v1) v5))
(assert (or (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v9 v12))
(assert (or v3 v3 (= v1 v5 v5 false v9 v10 v11 v16 v4 v1)))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v3))
(assert (or v1 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15)))
(assert (or v7 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v12))
(assert (or v15 v6 v15))
(assert (or (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v1 v5))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v3 v16))
(assert (or v14 v6 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4)))
(assert (or v14 v6 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15)))
(assert (or (= v1 v5 v5 (bvugt #b1101001101 #b1101001101) v9 v10 v11 v16 v4 v1) (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 (bvugt #b1101001101 #b1101001101) v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 (bvugt #b1101001101 #b1101001101) v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 (bvugt #b1101001101 #b1101001101) v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 (bvugt #b1101001101 #b1101001101) v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15)))
(assert (or (= v1 v5 v5 false v9 v10 v11 v16 v4 v1) v16 v7))
(assert (or v13 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v6))
(assert (or v15 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4)))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v14))
(assert (or (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v12 v6))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v12 v15))
(assert (or v13 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4)))
(assert (or (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v13 v16))
(assert v0)
(assert (or v7 (= v1 v5 v5 true v9 v10 v11 v16 v4 v1)))
(assert (or (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v7))
(assert (or v9 v14 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15)))
(assert (or (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v1 v7))
(assert (or (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v5 v1))
(assert (or v1 v13 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4)))
(assert (or v14 v3 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15)))
(assert (or (= v1 v5 v5 false v9 v10 v11 v16 v4 v1) v9 v1))
(assert (or (= v1 v5 v5 false v9 v10 v11 v16 v4 v1) v9 v12))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) (= v1 v5 v5 true v9 v10 v11 v16 v4 v1)))
(assert (or v14 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v15))
(assert (or v15 (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v5))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v7 v16))
(assert (or (xor v14 v20 v8 v9 v1 v0 v3 v10 v15) v6 v3))
(assert (or v13 (xor v14 v20 v8 v9 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v0 v3 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v15) v15))
(assert (or v16 (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4)))
(assert (or (xor v1 (xor v10 v12 v1 v2 true v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v13 v9))
(assert (or v13 v1 (= v1 v5 v5 false v9 v10 v11 v16 v4 v1)))
(assert (or (xor v1 (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11) v7 v4 v14 v9 v15 v4) v12))
(assert (or v6 (xor v1 v10 v7 v4 v14 v9 v15 v4)))
(assert (xor v10 v12 v1 v2 false v4 v3 v0 v12 v11))
(assert (or v14 (xor v1 false v7 v4 v14 v9 v15 v4)))
(assert (or v1 v9 v1))
(check-sat)

sat
failed to verify: (let ((a!1 (xor v1
                v10
                v12
                v1
                v2
                (bvugt #b1101001101 #b1101001101)
                v4
                v3
                v0
                v12
                v11
                v7
...
v15 |-> 22
v0 |-> 83
(error "line 75 column 10: an invalid model was generated")