; EXPECT: sat
(set-logic HO_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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback