1 2 3 4 5 6 7 8
(benchmark ite_real_valid :logic QF_LRA :status unsat :extrafuns ((x Real)) :extrapreds ((b)) :formula (not (implies (= x (ite b 0 1)) (>= x 0))) )