Last change
on this file since 76 was
12,
checked in by cecile, 13 years ago
|
cusp added
|
-
Property svn:executable set to
*
|
File size:
538 bytes
|
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 unsat |
---|
| 5 | :difficulty { 1 } |
---|
| 6 | :category { check } |
---|
| 7 | :logic QF_IDL |
---|
| 8 | :extrafuns ((x1 Int)) |
---|
| 9 | :extrafuns ((x2 Int)) |
---|
| 10 | :extrafuns ((x3 Int)) |
---|
| 11 | :extrafuns ((x4 Int)) |
---|
| 12 | :formula |
---|
| 13 | (and (<= (- x1 x2) 1000000000000000000000000000000000) |
---|
| 14 | (<= (- x2 x3) 2000000000000000000000000000000011) |
---|
| 15 | (<= (- x3 x4) (~ 1000000000000000000000000000000000)) |
---|
| 16 | (<= (- x4 x1) (~ 2000000000000000000000000000000012)))) |
---|
Note: See
TracBrowser
for help on using the repository browser.