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

(set-option :incremental false)
(set-info :status unsat)
(set-info :category "crafted")
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x () U)
(declare-fun y () U)
(declare-fun f (U) Bool)
(check-sat-assuming ( (let ((_let_0 (f x))) (let ((_let_1 (f y))) (and _let_0 (= _let_0 _let_1) (not _let_1)))) ))