summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith/delta-minimized-row-vector-bug.smt
blob: 5cf44c94efae151093883a07aae00ee61f0f6265 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

(benchmark delta_minimized_row_vector_bug.smt
:logic QF_LRA
:extrafuns ((x_120 Real))
:extrafuns ((x_11 Real))
:extrafuns ((x_102 Real))
:status sat
:formula
  (and (>= x_11 0)
    (or (= x_120 x_102) (<= x_102 (~ x_11)) (= x_120 (+ x_102 x_11) ))
  )

)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback