Add type to uninterpreted constant values (#8891)
[cvc5.git] / test / regress / cli / regress0 / ite.smt2
1 (set-logic QF_UF)
2 (set-info :status unsat)
3 (declare-sort U 0)
4 (declare-fun x () U)
5 (declare-fun y () U)
6 (assert (not (= x (ite true x y))))
7 (check-sat)