path: root/test/regress/regress0/simple.smtv1.smt2

(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x0 () Bool)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(check-sat-assuming ( (and (or x1 (not x0)) (or x0 (not x3)) (or x3 x2) (not x1) x2 x3) ))