(set-info :smt-lib-version 2.6)
(set-logic QF_LIA)
(set-info :source |
Generated by: Martin Bromberger
Generated on: 2018-01-06
Application: This is a problem with unbounded directions and, therefore, a good test for the termination/completeness of branch-and-bound solvers.
Publications: M. Bromberger. A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. (Work in progress.)

The benchmarks in this class are based on the problems from SMT-LIB/QF_LIA/CAV_2009 and SMT-LIB/QF_LIA/cut_lemmas.
I just replaced all variables x with x_+ - x_-, where x_+ and x_- are two new variables such that x_+, x_- >= 0.
This transformation is equisatisfiable.
The new variables and an unsatisfiable status guarantee that there are bounded and unbounded directions.
Target solver: CVC4 Mathsat SPASS-IQ YICES Z3
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun x9_plus () Int)
(declare-fun x9_minus () Int)
(declare-fun x8_plus () Int)
(declare-fun x8_minus () Int)
(declare-fun x7_plus () Int)
(declare-fun x7_minus () Int)
(declare-fun x6_plus () Int)
(declare-fun x6_minus () Int)
(declare-fun x4_plus () Int)
(declare-fun x4_minus () Int)
(declare-fun x3_plus () Int)
(declare-fun x3_minus () Int)
(declare-fun x1_plus () Int)
(declare-fun x1_minus () Int)
(declare-fun x0_plus () Int)
(declare-fun x0_minus () Int)
(declare-fun x5_plus () Int)
(declare-fun x5_minus () Int)
(declare-fun x2_plus () Int)
(declare-fun x2_minus () Int)
(assert (>= x9_plus 0))
(assert (>= x9_minus 0))
(assert (>= x8_plus 0))
(assert (>= x8_minus 0))
(assert (>= x7_plus 0))
(assert (>= x7_minus 0))
(assert (>= x6_plus 0))
(assert (>= x6_minus 0))
(assert (>= x4_plus 0))
(assert (>= x4_minus 0))
(assert (>= x3_plus 0))
(assert (>= x3_minus 0))
(assert (>= x1_plus 0))
(assert (>= x1_minus 0))
(assert (>= x0_plus 0))
(assert (>= x0_minus 0))
(assert (>= x5_plus 0))
(assert (>= x5_minus 0))
(assert (>= x2_plus 0))
(assert (>= x2_minus 0))
(assert (<= (+ (* 11 x9_plus) (* (- 11) x9_minus) (* 108 x8_plus) (* (- 108) x8_minus) (* 69 x7_plus) (* (- 69) x7_minus) (* 76 x6_plus) (* (- 76) x6_minus) (* 66 x4_plus) (* (- 66) x4_minus) (* (- 53) x3_plus) (* 53 x3_minus) (* 91 x1_plus) (* (- 91) x1_minus) (* 61 x0_plus) (* (- 61) x0_minus) ) (- 37) ) )
(assert (<= (+ (* 18 x9_plus) (* (- 18) x9_minus) (* 21 x8_plus) (* (- 21) x8_minus) (* 43 x7_plus) (* (- 43) x7_minus) (* 22 x5_plus) (* (- 22) x5_minus) (* (- 62) x3_plus) (* 62 x3_minus) (* 66 x2_plus) (* (- 66) x2_minus) (* (- 156) x1_plus) (* 156 x1_minus) ) (- 41) ) )
(assert (<= (+ (* 63 x9_plus) (* (- 63) x9_minus) (* (- 43) x7_plus) (* 43 x7_minus) (* 60 x6_plus) (* (- 60) x6_minus) (* 87 x5_plus) (* (- 87) x5_minus) (* 73 x2_plus) (* (- 73) x2_minus) (* 68 x1_plus) (* (- 68) x1_minus) (* 54 x0_plus) (* (- 54) x0_minus) ) (- 86) ) )
(assert (<= (+ (* 41 x9_plus) (* (- 41) x9_minus) (* (- 11) x8_plus) (* 11 x8_minus) (* (- 49) x6_plus) (* 49 x6_minus) (* (- 18) x5_plus) (* 18 x5_minus) (* (- 24) x4_plus) (* 24 x4_minus) (* 103 x3_plus) (* (- 103) x3_minus) (* (- 42) x1_plus) (* 42 x1_minus) ) (- 41) ) )
(assert (<= (+ (* 57 x9_plus) (* (- 57) x9_minus) (* (- 80) x8_plus) (* 80 x8_minus) (* 34 x7_plus) (* (- 34) x7_minus) (* (- 92) x3_plus) (* 92 x3_minus) (* 4 x2_plus) (* (- 4) x2_minus) (* (- 45) x1_plus) (* 45 x1_minus) (* 6 x0_plus) (* (- 6) x0_minus) ) (- 68) ) )
(assert (<= (+ (* 116 x7_plus) (* (- 116) x7_minus) (* 60 x5_plus) (* (- 60) x5_minus) (* (- 57) x4_plus) (* 57 x4_minus) (* (- 104) x3_plus) (* 104 x3_minus) (* 6 x2_plus) (* (- 6) x2_minus) (* 95 x1_plus) (* (- 95) x1_minus) (* (- 86) x0_plus) (* 86 x0_minus) ) 14 ) )
(assert (<= (+ (* 72 x9_plus) (* (- 72) x9_minus) (* 54 x8_plus) (* (- 54) x8_minus) (* (- 11) x7_plus) (* 11 x7_minus) (* (- 16) x6_plus) (* 16 x6_minus) (* 5 x5_plus) (* (- 5) x5_minus) (* (- 207) x1_plus) (* 207 x1_minus) ) 75 ) )
(assert (<= (+ x9_plus (* (- 1) x9_minus) (* 53 x7_plus) (* (- 53) x7_minus) (* (- 29) x6_plus) (* 29 x6_minus) (* 45 x5_plus) (* (- 45) x5_minus) (* (- 97) x4_plus) (* 97 x4_minus) (* 56 x0_plus) (* (- 56) x0_minus) ) (- 1) ) )
(assert (<= (+ (* 138 x6_plus) (* (- 138) x6_minus) (* 42 x5_plus) (* (- 42) x5_minus) (* (- 39) x4_plus) (* 39 x4_minus) (* 131 x3_plus) (* (- 131) x3_minus) (* (- 38) x2_plus) (* 38 x2_minus) (* (- 39) x1_plus) (* 39 x1_minus) ) (- 30) ) )
(assert (<= (+ (* 11 x9_plus) (* (- 11) x9_minus) (* 26 x8_plus) (* (- 26) x8_minus) (* (- 80) x6_plus) (* 80 x6_minus) (* (- 65) x5_plus) (* 65 x5_minus) (* 64 x1_plus) (* (- 64) x1_minus) ) (- 63) ) )
(assert (>= (+ (* 43 x8_plus) (* (- 43) x8_minus) (* (- 12) x7_plus) (* 12 x7_minus) (* 56 x6_plus) (* (- 56) x6_minus) (* (- 25) x4_plus) (* 25 x4_minus) (* (- 55) x3_plus) (* 55 x3_minus) (* 36 x1_plus) (* (- 36) x1_minus) (* (- 22) x0_plus) (* 22 x0_minus) ) (- 73) ) )
(assert (>= (+ (* 166 x8_plus) (* (- 166) x8_minus) (* (- 48) x7_plus) (* 48 x7_minus) (* (- 71) x5_plus) (* 71 x5_minus) (* 63 x3_plus) (* (- 63) x3_minus) (* (- 43) x2_plus) (* 43 x2_minus) (* (- 28) x1_plus) (* 28 x1_minus) (* (- 129) x0_plus) (* 129 x0_minus) ) 33 ) )
(assert (>= (+ (* 2 x9_plus) (* (- 2) x9_minus) (* (- 29) x7_plus) (* 29 x7_minus) (* 123 x6_plus) (* (- 123) x6_minus) (* 44 x5_plus) (* (- 44) x5_minus) (* (- 118) x2_plus) (* 118 x2_minus) (* (- 49) x1_plus) (* 49 x1_minus) (* 40 x0_plus) (* (- 40) x0_minus) ) 12 ) )
(assert (>= (+ (* 126 x9_plus) (* (- 126) x9_minus) (* 32 x7_plus) (* (- 32) x7_minus) (* (- 98) x5_plus) (* 98 x5_minus) (* (- 21) x4_plus) (* 21 x4_minus) (* (- 41) x3_plus) (* 41 x3_minus) (* 49 x2_plus) (* (- 49) x2_minus) ) 77 ) )
(assert (>= (+ (* 99 x6_plus) (* (- 99) x6_minus) (* 31 x5_plus) (* (- 31) x5_minus) (* (- 34) x3_plus) (* 34 x3_minus) (* (- 61) x2_plus) (* 61 x2_minus) (* (- 103) x1_plus) (* 103 x1_minus) (* (- 2) x0_plus) (* 2 x0_minus) ) (- 9) ) )
(assert (>= (+ (* 200 x9_plus) (* (- 200) x9_minus) (* (- 3) x8_plus) (* 3 x8_minus) (* (- 53) x5_plus) (* 53 x5_minus) (* (- 85) x3_plus) (* 85 x3_minus) (* 119 x2_plus) (* (- 119) x2_minus) (* (- 87) x0_plus) (* 87 x0_minus) ) (- 8) ) )
(assert (>= (+ (* 17 x9_plus) (* (- 17) x9_minus) (* 22 x8_plus) (* (- 22) x8_minus) (* 20 x7_plus) (* (- 20) x7_minus) (* (- 22) x6_plus) (* 22 x6_minus) (* (- 155) x5_plus) (* 155 x5_minus) (* 13 x2_plus) (* (- 13) x2_minus) ) (- 86) ) )
(assert (>= (+ (* 59 x9_plus) (* (- 59) x9_minus) (* 13 x7_plus) (* (- 13) x7_minus) (* (- 34) x4_plus) (* 34 x4_minus) (* (- 45) x3_plus) (* 45 x3_minus) (* 81 x2_plus) (* (- 81) x2_minus) (* 67 x0_plus) (* (- 67) x0_minus) ) (- 61) ) )
(assert (>= (+ (* 44 x9_plus) (* (- 44) x9_minus) (* (- 110) x8_plus) (* 110 x8_minus) (* 3 x7_plus) (* (- 3) x7_minus) (* 36 x3_plus) (* (- 36) x3_minus) (* (- 32) x1_plus) (* 32 x1_minus) (* 33 x0_plus) (* (- 33) x0_minus) ) (- 89) ) )
(assert (>= (+ (* 81 x8_plus) (* (- 81) x8_minus) (* 136 x7_plus) (* (- 136) x7_minus) (* 38 x4_plus) (* (- 38) x4_minus) (* (- 36) x2_plus) (* 36 x2_minus) (* 113 x0_plus) (* (- 113) x0_minus) ) 28 ) )
(check-sat)
(exit)