test/regress/regress0/buggy-ite.smt2

   1 ; This was causing trouble in CVC4 r1434 due to mishandling of ITE
   2 ; removal for PARAMETERIZED kinds.
   3 ; Thanks to Andrew Reynolds for catching this.
   4 (set-logic QF_UF)
   5 (set-info :smt-lib-version 2.0)
   6 (set-info :status sat)
   7 (declare-sort U 0)
   8 (declare-fun a () U)
   9 (declare-fun c () Bool)
  10 (declare-fun g (U) Bool)
  11 (assert (g (ite c a a)))
  12 (check-sat)
  13 (exit)