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