(set-option :produce-models true) (get-option :produce-models) (set-logic QF_UF) (declare-fun a () Bool) (declare-fun b () Bool) (assert (or a b)) (assert (not (and a b))) (check-sat) (get-model)