summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug164.smt
blob: c992b7f1f8bfbc83d3555b60f13cdefb900fd142 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

(benchmark Carpark2_t1_1.smt
:logic QF_LRA
:extrafuns ((x_34 Real))
:extrafuns ((x_13 Real))
:extrafuns ((x_30 Real))
:extrafuns ((x_59 Real))
:status unsat
:formula
(and (not (<= x_59 0))
     (= x_30 x_59)
     (= x_30 0)
     (or true (= x_13 x_34)))
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback