path: root/test/regress/regress0/uf/bug217.smt2

(set-logic QF_UF)
(set-info :status unsat)
(declare-fun f (Bool) Bool)
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)
;(assert (and x (or (f x) (f y))))
(assert (or (f x) (f y) (f z)))
(assert (not (f false)))
(assert (not (f true)))
(check-sat)
;(get-value ((f true) (f false) (f x) (f y) (f z) x y z))