path: root/test/regress/regress0/uf/NEQ016_size5_reduced2b.smtv1.smt2

(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun p4 (U) Bool)
(declare-fun c_4 () U)
(declare-fun c7 () U)
(declare-fun c_0 () U)
(check-sat-assuming ( (and (not (p4 c_0)) (p4 c7) (= c_0 c7)) ))