Last change
on this file since 106 was
12,
checked in by cecile, 13 years ago
|
cusp added
|
-
Property svn:executable set to
*
|
File size:
390 bytes
|
Rev | Line | |
---|
[12] | 1 | (benchmark int_incompleteness1.smt |
---|
| 2 | :source { Leonardo de Moura } |
---|
| 3 | :notes "This benchmark is designed to check if the integer DP is complete." |
---|
| 4 | :status unsat |
---|
| 5 | :difficulty { 0 } |
---|
| 6 | :category { check } |
---|
| 7 | :logic QF_IDL |
---|
| 8 | :extrafuns ((x1 Int) (x2 Int)) |
---|
| 9 | :formula |
---|
| 10 | (and (> (- x1 x2) 0) |
---|
| 11 | (< (- x1 x2) 4) |
---|
| 12 | (not (= (- x1 x2) 1)) |
---|
| 13 | (not (= (- x1 x2) 2)) |
---|
| 14 | (not (= (- x1 x2) 3)))) |
---|
| 15 | |
---|
| 16 | |
---|
| 17 | |
---|
| 18 | |
---|
Note: See
TracBrowser
for help on using the repository browser.