Variable elimination in Z3

Question

After solving a constraint system using z3 I get a model where some variables are set to None (I'm using Pyz3). Does it mean that those variables have been eliminated?

Thanks!

Answer 1

Unassigned variables should be interpreted as "don't cares". That is, any assignment would satisfy the input formula. Here is a small example (also available here). The assignment produced by Z3 only assigns x to 1. The value of y doesn't matter.

(set-option :auto-config false)
(declare-const x Int)
(declare-const y Int)
(assert (or (= x 1) (= y 1)))
(check-sat)
(get-model)