summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uflra/bug449.smt
blob: 91bb5fb486ed3fa6aacf177e7bf4d1b790ecc4d8 (plain) 
1
2
3
4
5
6
7
8
9
10
11

(benchmark fuzzsmt
:logic QF_UFLRA
:extrapreds ((p0 Real))
:extrafuns ((v0 Real))
:status sat
:formula
(and
     (p0 v0)
     (< v0 0)
     (not (p0 (- 1)))
))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback