(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 sat)
(declare-fun x9_plus () Int)
(declare-fun x9_minus () Int)
(declare-fun x7_plus () Int)
(declare-fun x7_minus () Int)
(declare-fun x6_plus () Int)
(declare-fun x6_minus () Int)
(declare-fun x5_plus () Int)
(declare-fun x5_minus () Int)
(declare-fun x4_plus () Int)
(declare-fun x4_minus () Int)
(declare-fun x2_plus () Int)
(declare-fun x2_minus () Int)
(declare-fun x1_plus () Int)
(declare-fun x1_minus () Int)
(declare-fun x0_plus () Int)
(declare-fun x0_minus () Int)
(declare-fun x3_plus () Int)
(declare-fun x3_minus () Int)
(declare-fun x8_plus () Int)
(declare-fun x8_minus () Int)
(assert (>= x9_plus 0))
(assert (>= x9_minus 0))
(assert (>= x7_plus 0))
(assert (>= x7_minus 0))
(assert (>= x6_plus 0))
(assert (>= x6_minus 0))
(assert (>= x5_plus 0))
(assert (>= x5_minus 0))
(assert (>= x4_plus 0))
(assert (>= x4_minus 0))
(assert (>= x2_plus 0))
(assert (>= x2_minus 0))
(assert (>= x1_plus 0))
(assert (>= x1_minus 0))
(assert (>= x0_plus 0))
(assert (>= x0_minus 0))
(assert (>= x3_plus 0))
(assert (>= x3_minus 0))
(assert (>= x8_plus 0))
(assert (>= x8_minus 0))
(assert (<= (+ (* 49 x9_plus) (* (- 49) x9_minus) (* 3 x7_plus) (* (- 3) x7_minus) (* 179 x6_plus) (* (- 179) x6_minus) (* (- 52) x5_plus) (* 52 x5_minus) (* (- 8) x4_plus) (* 8 x4_minus) (* 19 x2_plus) (* (- 19) x2_minus) (* 69 x1_plus) (* (- 69) x1_minus) (* (- 53) x0_plus) (* 53 x0_minus) ) 65 ) )
(assert (<= (+ (* 69 x9_plus) (* (- 69) x9_minus) (* (- 40) x7_plus) (* 40 x7_minus) (* (- 122) x6_plus) (* 122 x6_minus) (* 75 x4_plus) (* (- 75) x4_minus) (* 93 x3_plus) (* (- 93) x3_minus) (* 77 x2_plus) (* (- 77) x2_minus) (* 81 x1_plus) (* (- 81) x1_minus) (* 38 x0_plus) (* (- 38) x0_minus) ) (- 1) ) )
(assert (<= (+ (* 96 x9_plus) (* (- 96) x9_minus) (* (- 51) x8_plus) (* 51 x8_minus) (* 2 x6_plus) (* (- 2) x6_minus) (* (- 11) x5_plus) (* 11 x5_minus) (* 62 x3_plus) (* (- 62) x3_minus) (* 113 x2_plus) (* (- 113) x2_minus) (* 99 x0_plus) (* (- 99) x0_minus) ) 49 ) )
(assert (<= (+ (* 90 x9_plus) (* (- 90) x9_minus) (* 52 x8_plus) (* (- 52) x8_minus) (* (- 12) x6_plus) (* 12 x6_minus) (* (- 90) x5_plus) (* 90 x5_minus) (* 18 x4_plus) (* (- 18) x4_minus) (* 49 x2_plus) (* (- 49) x2_minus) (* 32 x0_plus) (* (- 32) x0_minus) ) (- 8) ) )
(assert (<= (+ (* 35 x8_plus) (* (- 35) x8_minus) (* 23 x7_plus) (* (- 23) x7_minus) (* 62 x6_plus) (* (- 62) x6_minus) (* 95 x5_plus) (* (- 95) x5_minus) (* 65 x3_plus) (* (- 65) x3_minus) (* (- 41) x2_plus) (* 41 x2_minus) (* 23 x1_plus) (* (- 23) x1_minus) ) (- 53) ) )
(assert (<= (+ (* 24 x8_plus) (* (- 24) x8_minus) (* 73 x7_plus) (* (- 73) x7_minus) (* (- 83) x6_plus) (* 83 x6_minus) (* (- 74) x4_plus) (* 74 x4_minus) (* 34 x3_plus) (* (- 34) x3_minus) (* (- 150) x0_plus) (* 150 x0_minus) ) 93 ) )
(assert (<= (+ (* 83 x9_plus) (* (- 83) x9_minus) (* 75 x8_plus) (* (- 75) x8_minus) (* 66 x7_plus) (* (- 66) x7_minus) (* (- 11) x6_plus) (* 11 x6_minus) (* 29 x4_plus) (* (- 29) x4_minus) (* 52 x0_plus) (* (- 52) x0_minus) ) 86 ) )
(assert (<= (+ (* 57 x8_plus) (* (- 57) x8_minus) (* (- 43) x6_plus) (* 43 x6_minus) (* 171 x4_plus) (* (- 171) x4_minus) (* 3 x2_plus) (* (- 3) x2_minus) (* (- 17) x1_plus) (* 17 x1_minus) (* (- 61) x0_plus) (* 61 x0_minus) ) 19 ) )
(assert (<= (+ (* 70 x9_plus) (* (- 70) x9_minus) (* (- 79) x7_plus) (* 79 x7_minus) (* (- 87) x6_plus) (* 87 x6_minus) (* (- 50) x3_plus) (* 50 x3_minus) (* 52 x2_plus) (* (- 52) x2_minus) (* 24 x1_plus) (* (- 24) x1_minus) ) 37 ) )
(assert (<= (+ (* 15 x9_plus) (* (- 15) x9_minus) (* (- 81) x8_plus) (* 81 x8_minus) (* 59 x3_plus) (* (- 59) x3_minus) (* 45 x1_plus) (* (- 45) x1_minus) (* 79 x0_plus) (* (- 79) x0_minus) ) 0 ) )
(assert (<= (+ (* 75 x8_plus) (* (- 75) x8_minus) (* 19 x6_plus) (* (- 19) x6_minus) (* 25 x5_plus) (* (- 25) x5_minus) (* (- 64) x4_plus) (* 64 x4_minus) (* 228 x1_plus) (* (- 228) x1_minus) ) 81 ) )
(assert (>= (+ (* 103 x8_plus) (* (- 103) x8_minus) (* (- 90) x7_plus) (* 90 x7_minus) (* 20 x6_plus) (* (- 20) x6_minus) (* (- 78) x5_plus) (* 78 x5_minus) (* (- 5) x4_plus) (* 5 x4_minus) (* (- 38) x3_plus) (* 38 x3_minus) (* (- 49) x1_plus) (* 49 x1_minus) (* 11 x0_plus) (* (- 11) x0_minus) ) 60 ) )
(assert (>= (+ (* 55 x7_plus) (* (- 55) x7_minus) (* 91 x6_plus) (* (- 91) x6_minus) (* 69 x5_plus) (* (- 69) x5_minus) (* 75 x4_plus) (* (- 75) x4_minus) (* (- 52) x3_plus) (* 52 x3_minus) (* 13 x2_plus) (* (- 13) x2_minus) (* 101 x1_plus) (* (- 101) x1_minus) (* 53 x0_plus) (* (- 53) x0_minus) ) 94 ) )
(assert (>= (+ (* 52 x9_plus) (* (- 52) x9_minus) (* (- 17) x8_plus) (* 17 x8_minus) (* (- 32) x6_plus) (* 32 x6_minus) (* 76 x4_plus) (* (- 76) x4_minus) (* (- 20) x3_plus) (* 20 x3_minus) (* (- 105) x2_plus) (* 105 x2_minus) (* (- 58) x0_plus) (* 58 x0_minus) ) 64 ) )
(assert (>= (+ (* 4 x9_plus) (* (- 4) x9_minus) (* (- 24) x6_plus) (* 24 x6_minus) (* 86 x5_plus) (* (- 86) x5_minus) (* (- 96) x3_plus) (* 96 x3_minus) x2_plus (* (- 1) x2_minus) (* (- 137) x1_plus) (* 137 x1_minus) (* 78 x0_plus) (* (- 78) x0_minus) ) (- 16) ) )
(assert (>= (+ (* 163 x9_plus) (* (- 163) x9_minus) (* 95 x6_plus) (* (- 95) x6_minus) (* 14 x5_plus) (* (- 14) x5_minus) (* (- 27) x4_plus) (* 27 x4_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* (- 30) x0_plus) (* 30 x0_minus) ) 2 ) )
(assert (>= (+ (* 50 x7_plus) (* (- 50) x7_minus) (* 53 x6_plus) (* (- 53) x6_minus) (* 11 x5_plus) (* (- 11) x5_minus) (* (- 22) x3_plus) (* 22 x3_minus) (* (- 26) x2_plus) (* 26 x2_minus) (* 23 x1_plus) (* (- 23) x1_minus) ) 99 ) )
(assert (>= (+ (* 46 x8_plus) (* (- 46) x8_minus) (* 87 x6_plus) (* (- 87) x6_minus) x5_plus (* (- 1) x5_minus) (* (- 153) x3_plus) (* 153 x3_minus) (* (- 100) x1_plus) (* 100 x1_minus) (* 4 x0_plus) (* (- 4) x0_minus) ) (- 41) ) )
(assert (>= (+ (* 67 x9_plus) (* (- 67) x9_minus) (* 75 x8_plus) (* (- 75) x8_minus) (* 18 x7_plus) (* (- 18) x7_minus) (* 38 x6_plus) (* (- 38) x6_minus) (* 26 x3_plus) (* (- 26) x3_minus) (* 95 x2_plus) (* (- 95) x2_minus) ) (- 2) ) )
(assert (>= (+ (* 73 x8_plus) (* (- 73) x8_minus) (* (- 88) x7_plus) (* 88 x7_minus) (* 19 x6_plus) (* (- 19) x6_minus) (* (- 3) x5_plus) (* 3 x5_minus) (* (- 147) x3_plus) (* 147 x3_minus) (* (- 8) x2_plus) (* 8 x2_minus) ) (- 89) ) )
(check-sat)
(exit)