1 2 3 4 5 6 7 8 9 10 11 12
; EXPECT: unsat (set-logic HO_ALL) (set-info :status unsat) (declare-fun f (Int Int) Int) (declare-fun a () Int) (declare-fun b () Int) (assert (forall ((x (-> Int Int)) (y Int)) (not (= (x y) 0)))) (assert (= (f a b) 0)) (check-sat)