summaryrefslogtreecommitdiff
path: root/test/regress/regress0/ite_real_valid.smt
blob: eeaaa17e0f657a83c739734cb8b05106f2c845bd (plain) 
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)))
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback