1 2 3 4 5 6 7 8 9 10 11 12 13 14
; COMMAND-LINE: --uf-ho ; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun f (Int Int) Int) (declare-fun g (Int) (-> Int Int)) (declare-fun h () (-> Int Int Int)) (assert (and (= f g) (= g h))) (assert (= (f 1 2) 5)) (assert (= (f 2 1) 7)) (check-sat)