(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 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 x5_plus () Int)
(declare-fun x5_minus () Int)
(declare-fun x3_plus () Int)
(declare-fun x3_minus () Int)
(declare-fun x2_plus () Int)
(declare-fun x2_minus () Int)
(declare-fun x1_plus () Int)
(declare-fun x1_minus () Int)
(declare-fun x4_plus () Int)
(declare-fun x4_minus () Int)
(declare-fun x0_plus () Int)
(declare-fun x0_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 (>= x5_plus 0))
(assert (>= x5_minus 0))
(assert (>= x3_plus 0))
(assert (>= x3_minus 0))
(assert (>= x2_plus 0))
(assert (>= x2_minus 0))
(assert (>= x1_plus 0))
(assert (>= x1_minus 0))
(assert (>= x4_plus 0))
(assert (>= x4_minus 0))
(assert (>= x0_plus 0))
(assert (>= x0_minus 0))
(assert (<= (+ (* 13 x9_plus) (* (- 13) x9_minus) (* 18 x8_plus) (* (- 18) x8_minus) (* (- 4) x7_plus) (* 4 x7_minus) (* (- 42) x6_plus) (* 42 x6_minus) (* 32 x5_plus) (* (- 32) x5_minus) (* 40 x3_plus) (* (- 40) x3_minus) (* (- 11) x2_plus) (* 11 x2_minus) (* 14 x1_plus) (* (- 14) x1_minus) ) (- 9) ) )
(assert (<= (+ (* 40 x9_plus) (* (- 40) x9_minus) (* (- 44) x7_plus) (* 44 x7_minus) (* 60 x6_plus) (* (- 60) x6_minus) (* (- 62) x5_plus) (* 62 x5_minus) (* 74 x4_plus) (* (- 74) x4_minus) (* 59 x3_plus) (* (- 59) x3_minus) (* 40 x1_plus) (* (- 40) x1_minus) (* 19 x0_plus) (* (- 19) x0_minus) ) 30 ) )
(assert (<= (+ (* 113 x8_plus) (* (- 113) x8_minus) (* (- 82) x7_plus) (* 82 x7_minus) (* 85 x6_plus) (* (- 85) x6_minus) (* 79 x5_plus) (* (- 79) x5_minus) (* (- 73) x3_plus) (* 73 x3_minus) (* (- 21) x2_plus) (* 21 x2_minus) (* (- 85) x1_plus) (* 85 x1_minus) ) (- 63) ) )
(assert (<= (+ (* 89 x9_plus) (* (- 89) x9_minus) (* 75 x8_plus) (* (- 75) x8_minus) (* 135 x7_plus) (* (- 135) x7_minus) (* 37 x4_plus) (* (- 37) x4_minus) (* 90 x3_plus) (* (- 90) x3_minus) (* 69 x1_plus) (* (- 69) x1_minus) (* (- 132) x0_plus) (* 132 x0_minus) ) (- 32) ) )
(assert (<= (+ (* 35 x9_plus) (* (- 35) x9_minus) (* (- 39) x8_plus) (* 39 x8_minus) (* (- 53) x7_plus) (* 53 x7_minus) (* 19 x5_plus) (* (- 19) x5_minus) (* (- 44) x4_plus) (* 44 x4_minus) (* (- 85) x2_plus) (* 85 x2_minus) (* 32 x1_plus) (* (- 32) x1_minus) ) 72 ) )
(assert (<= (+ (* 43 x9_plus) (* (- 43) x9_minus) (* (- 115) x8_plus) (* 115 x8_minus) (* (- 5) x6_plus) (* 5 x6_minus) (* 81 x4_plus) (* (- 81) x4_minus) (* (- 39) x1_plus) (* 39 x1_minus) (* (- 135) x0_plus) (* 135 x0_minus) ) (- 35) ) )
(assert (<= (+ (* 27 x8_plus) (* (- 27) x8_minus) (* (- 37) x6_plus) (* 37 x6_minus) (* 106 x5_plus) (* (- 106) x5_minus) (* 17 x4_plus) (* (- 17) x4_minus) (* (- 76) x3_plus) (* 76 x3_minus) (* 73 x1_plus) (* (- 73) x1_minus) ) 75 ) )
(assert (<= (+ (* 7 x7_plus) (* (- 7) x7_minus) (* (- 30) x5_plus) (* 30 x5_minus) (* 118 x3_plus) (* (- 118) x3_minus) (* (- 7) x1_plus) (* 7 x1_minus) (* 33 x0_plus) (* (- 33) x0_minus) ) (- 41) ) )
(assert (<= (+ (* 45 x8_plus) (* (- 45) x8_minus) (* (- 20) x7_plus) (* 20 x7_minus) (* 141 x6_plus) (* (- 141) x6_minus) (* (- 3) x3_plus) (* 3 x3_minus) (* 157 x2_plus) (* (- 157) x2_minus) ) 77 ) )
(assert (<= (+ (* 9 x8_plus) (* (- 9) x8_minus) (* (- 10) x5_plus) (* 10 x5_minus) (* 161 x2_plus) (* (- 161) x2_minus) (* 32 x1_plus) (* (- 32) x1_minus) (* 9 x0_plus) (* (- 9) x0_minus) ) (- 87) ) )
(assert (<= (+ (* 71 x9_plus) (* (- 71) x9_minus) (* 83 x8_plus) (* (- 83) x8_minus) (* (- 88) x6_plus) (* 88 x6_minus) (* (- 76) x1_plus) (* 76 x1_minus) (* 23 x0_plus) (* (- 23) x0_minus) ) (- 34) ) )
(assert (<= (+ (* 64 x7_plus) (* (- 64) x7_minus) (* 59 x6_plus) (* (- 59) x6_minus) (* (- 39) x4_plus) (* 39 x4_minus) (* 34 x3_plus) (* (- 34) x3_minus) ) (- 16) ) )
(assert (>= (+ (* 15 x8_plus) (* (- 15) x8_minus) (* (- 66) x7_plus) (* 66 x7_minus) (* (- 73) x5_plus) (* 73 x5_minus) (* 79 x4_plus) (* (- 79) x4_minus) (* (- 11) x3_plus) (* 11 x3_minus) (* (- 83) x2_plus) (* 83 x2_minus) (* (- 34) x1_plus) (* 34 x1_minus) ) (- 4) ) )
(assert (>= (+ (* 12 x9_plus) (* (- 12) x9_minus) (* 28 x7_plus) (* (- 28) x7_minus) (* 43 x6_plus) (* (- 43) x6_minus) (* 2 x5_plus) (* (- 2) x5_minus) (* (- 81) x3_plus) (* 81 x3_minus) (* 16 x2_plus) (* (- 16) x2_minus) (* 45 x1_plus) (* (- 45) x1_minus) ) 15 ) )
(assert (>= (+ (* 17 x9_plus) (* (- 17) x9_minus) (* (- 95) x6_plus) (* 95 x6_minus) (* (- 73) x5_plus) (* 73 x5_minus) (* 57 x4_plus) (* (- 57) x4_minus) (* (- 3) x3_plus) (* 3 x3_minus) (* 44 x2_plus) (* (- 44) x2_minus) (* (- 19) x0_plus) (* 19 x0_minus) ) 8 ) )
(assert (>= (+ (* 71 x9_plus) (* (- 71) x9_minus) (* 16 x8_plus) (* (- 16) x8_minus) (* (- 138) x7_plus) (* 138 x7_minus) (* 57 x6_plus) (* (- 57) x6_minus) (* (- 66) x5_plus) (* 66 x5_minus) (* 5 x4_plus) (* (- 5) x4_minus) (* 7 x0_plus) (* (- 7) x0_minus) ) 87 ) )
(assert (>= (+ (* 7 x9_plus) (* (- 7) x9_minus) (* 24 x6_plus) (* (- 24) x6_minus) (* 28 x4_plus) (* (- 28) x4_minus) (* (- 89) x3_plus) (* 89 x3_minus) (* 31 x2_plus) (* (- 31) x2_minus) (* (- 109) x0_plus) (* 109 x0_minus) ) 83 ) )
(assert (>= (+ (* 39 x9_plus) (* (- 39) x9_minus) (* 19 x6_plus) (* (- 19) x6_minus) (* 56 x5_plus) (* (- 56) x5_minus) (* (- 34) x4_plus) (* 34 x4_minus) (* (- 15) x3_plus) (* 15 x3_minus) (* 12 x0_plus) (* (- 12) x0_minus) ) 31 ) )
(assert (>= (+ (* 47 x9_plus) (* (- 47) x9_minus) (* (- 72) x6_plus) (* 72 x6_minus) (* 54 x5_plus) (* (- 54) x5_minus) (* (- 50) x4_plus) (* 50 x4_minus) (* 66 x3_plus) (* (- 66) x3_minus) (* 146 x0_plus) (* (- 146) x0_minus) ) 27 ) )
(assert (>= (+ (* 36 x9_plus) (* (- 36) x9_minus) (* (- 88) x6_plus) (* 88 x6_minus) (* (- 13) x5_plus) (* 13 x5_minus) (* (- 45) x3_plus) (* 45 x3_minus) (* (- 130) x1_plus) (* 130 x1_minus) ) (- 74) ) )
(check-sat)
(exit)