path: root/test/regress/regress0/ho/cong-full-apply.smt2

; COMMAND-LINE: --uf-ho
; EXPECT: unsat
(set-logic UFLIA)
(set-info :status unsat)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-fun h (Int) Int)

(assert (not (= (f 0) (g 0))))
(assert (not (= (f 0) (h 0))))
(assert (or (= f g) (= f h)))

(check-sat)