summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith/miplibtrick.smt
blob: 93cd6d219951cb841d3ce3200d4c8151c7c6d6cc (plain) 
1
2
3
4
5
6
7
8
9
10
11

(benchmark miplibtrick
  :status sat
  :logic QF_LRA
  :extrafuns ((tmp1 Real))
  :extrapreds ((x177))

  :formula( and
    ( implies ( and ( not x177 ) true ) ( = tmp1 0 ) )
    ( implies ( and x177 true ) ( = tmp1 (~ 350) ) )
  )
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback