test/regress/regress0/uf/euf_simp01.smtv1.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13

(set-option :incremental false)
(set-info :status sat)
(set-info :category "crafted")
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x () U)
(declare-fun y () U)
(declare-fun z () U)
(declare-fun f (U) U)
(declare-fun g (U) U)
(declare-fun H (U U) U)
(declare-fun J (U U) U)
(check-sat-assuming ( (and (= (f x) (f z)) (= (g y) (g z)) (or (not (= x z)) (not (= y z)))) ))