Rev | Line | |
---|
[12] | 1 | (benchmark bignum |
---|
| 2 | :source { SMT-COMP'06 Organizers } |
---|
| 3 | :notes "This benchmark is designed to check if the DP supports bignumbers." |
---|
| 4 | :status sat |
---|
| 5 | :difficulty { 2 } |
---|
| 6 | :category { check } |
---|
| 7 | :logic QF_RDL |
---|
| 8 | :extrafuns ((x1 Real)) |
---|
| 9 | :extrafuns ((x2 Real)) |
---|
| 10 | :extrafuns ((x3 Real)) |
---|
| 11 | :extrafuns ((x4 Real)) |
---|
| 12 | :formula |
---|
| 13 | (and (<= (- x1 x2) (/ 1 1000000000000000000000000000000000)) |
---|
| 14 | (<= (- x2 x3) (/ 1 2000000000000000000000000000000011)) |
---|
| 15 | (<= (- x3 x4) (~ (/ 1 1000000000000000000000000000000000))) |
---|
| 16 | (<= (- x4 x1) (~ (/ 1 2000000000000000000000000000000012))))) |
---|
Note: See
TracBrowser
for help on using the repository browser.