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)