(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 x0_plus () Int)
(declare-fun x0_minus () Int)
(declare-fun x4_plus () Int)
(declare-fun x4_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 (>= x0_plus 0))
(assert (>= x0_minus 0))
(assert (>= x4_plus 0))
(assert (>= x4_minus 0))
(assert (<= (+ (* 90 x9_plus) (* (- 90) x9_minus) (* (- 93) x8_plus) (* 93 x8_minus) (* (- 42) x7_plus) (* 42 x7_minus) (* (- 72) x6_plus) (* 72 x6_minus) (* (- 41) x5_plus) (* 41 x5_minus) (* 8 x3_plus) (* (- 8) x3_minus) (* 95 x2_plus) (* (- 95) x2_minus) (* (- 92) x1_plus) (* 92 x1_minus) (* 10 x0_plus) (* (- 10) x0_minus) ) 32 ) )
(assert (<= (+ (* 3 x9_plus) (* (- 3) x9_minus) (* 83 x8_plus) (* (- 83) x8_minus) (* (- 25) x6_plus) (* 25 x6_minus) (* 73 x4_plus) (* (- 73) x4_minus) (* (- 23) x3_plus) (* 23 x3_minus) (* (- 25) x2_plus) (* 25 x2_minus) (* 94 x1_plus) (* (- 94) x1_minus) (* 53 x0_plus) (* (- 53) x0_minus) ) 16 ) )
(assert (<= (+ (* 83 x9_plus) (* (- 83) x9_minus) (* (- 12) x8_plus) (* 12 x8_minus) (* 57 x4_plus) (* (- 57) x4_minus) (* 41 x3_plus) (* (- 41) x3_minus) (* (- 39) x2_plus) (* 39 x2_minus) (* (- 60) x1_plus) (* 60 x1_minus) (* (- 58) x0_plus) (* 58 x0_minus) ) (- 28) ) )
(assert (<= (+ (* 29 x8_plus) (* (- 29) x8_minus) (* 94 x7_plus) (* (- 94) x7_minus) (* (- 40) x6_plus) (* 40 x6_minus) (* 107 x5_plus) (* (- 107) x5_minus) (* 82 x2_plus) (* (- 82) x2_minus) (* 78 x1_plus) (* (- 78) x1_minus) (* (- 11) x0_plus) (* 11 x0_minus) ) 6 ) )
(assert (<= (+ (* 67 x9_plus) (* (- 67) x9_minus) (* 64 x6_plus) (* (- 64) x6_minus) (* (- 79) x5_plus) (* 79 x5_minus) (* (- 17) x4_plus) (* 17 x4_minus) (* (- 69) x3_plus) (* 69 x3_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* 3 x1_plus) (* (- 3) x1_minus) ) 60 ) )
(assert (<= (+ (* 54 x9_plus) (* (- 54) x9_minus) (* 72 x8_plus) (* (- 72) x8_minus) (* 2 x5_plus) (* (- 2) x5_minus) (* (- 12) x4_plus) (* 12 x4_minus) (* 12 x3_plus) (* (- 12) x3_minus) (* 29 x1_plus) (* (- 29) x1_minus) ) (- 4) ) )
(assert (<= (+ (* 35 x9_plus) (* (- 35) x9_minus) (* (- 109) x7_plus) (* 109 x7_minus) (* (- 72) x5_plus) (* 72 x5_minus) (* (- 18) x3_plus) (* 18 x3_minus) (* (- 103) x2_plus) (* 103 x2_minus) (* (- 68) x1_plus) (* 68 x1_minus) ) 81 ) )
(assert (<= (+ (* 48 x9_plus) (* (- 48) x9_minus) (* 17 x4_plus) (* (- 17) x4_minus) (* 38 x2_plus) (* (- 38) x2_minus) (* 39 x1_plus) (* (- 39) x1_minus) (* (- 49) x0_plus) (* 49 x0_minus) ) (- 26) ) )
(assert (<= (+ (* 143 x6_plus) (* (- 143) x6_minus) (* 41 x4_plus) (* (- 41) x4_minus) (* (- 114) x2_plus) (* 114 x2_minus) (* (- 145) x1_plus) (* 145 x1_minus) ) (- 97) ) )
(assert (>= (+ (* 86 x9_plus) (* (- 86) x9_minus) (* (- 75) x6_plus) (* 75 x6_minus) (* 66 x5_plus) (* (- 66) x5_minus) (* (- 37) x4_plus) (* 37 x4_minus) (* 41 x3_plus) (* (- 41) x3_minus) (* (- 15) x2_plus) (* 15 x2_minus) (* 21 x1_plus) (* (- 21) x1_minus) (* (- 25) x0_plus) (* 25 x0_minus) ) (- 40) ) )
(assert (>= (+ (* 35 x9_plus) (* (- 35) x9_minus) (* (- 48) x8_plus) (* 48 x8_minus) (* (- 103) x7_plus) (* 103 x7_minus) (* 26 x6_plus) (* (- 26) x6_minus) (* (- 69) x5_plus) (* 69 x5_minus) (* (- 7) x4_plus) (* 7 x4_minus) (* 8 x3_plus) (* (- 8) x3_minus) (* (- 16) x1_plus) (* 16 x1_minus) ) 23 ) )
(assert (>= (+ (* 54 x9_plus) (* (- 54) x9_minus) (* (- 69) x8_plus) (* 69 x8_minus) (* (- 138) x7_plus) (* 138 x7_minus) (* 93 x6_plus) (* (- 93) x6_minus) (* (- 30) x5_plus) (* 30 x5_minus) (* (- 22) x4_plus) (* 22 x4_minus) (* 45 x2_plus) (* (- 45) x2_minus) (* (- 1) x0_plus) x0_minus ) (- 54) ) )
(assert (>= (+ (* 34 x8_plus) (* (- 34) x8_minus) (* (- 98) x6_plus) (* 98 x6_minus) (* 14 x5_plus) (* (- 14) x5_minus) (* (- 32) x4_plus) (* 32 x4_minus) (* 33 x3_plus) (* (- 33) x3_minus) (* 64 x2_plus) (* (- 64) x2_minus) (* 19 x0_plus) (* (- 19) x0_minus) ) 85 ) )
(assert (>= (+ x8_plus (* (- 1) x8_minus) (* 119 x7_plus) (* (- 119) x7_minus) (* (- 27) x5_plus) (* 27 x5_minus) (* (- 37) x4_plus) (* 37 x4_minus) (* 85 x3_plus) (* (- 85) x3_minus) (* 82 x1_plus) (* (- 82) x1_minus) (* (- 142) x0_plus) (* 142 x0_minus) ) (- 54) ) )
(assert (>= (+ (* 37 x8_plus) (* (- 37) x8_minus) (* (- 144) x7_plus) (* 144 x7_minus) (* 177 x6_plus) (* (- 177) x6_minus) (* 54 x5_plus) (* (- 54) x5_minus) (* 55 x3_plus) (* (- 55) x3_minus) (* (- 95) x1_plus) (* 95 x1_minus) ) (- 4) ) )
(assert (>= (+ (* 56 x9_plus) (* (- 56) x9_minus) (* (- 8) x8_plus) (* 8 x8_minus) (* 27 x7_plus) (* (- 27) x7_minus) (* 109 x5_plus) (* (- 109) x5_minus) (* 9 x3_plus) (* (- 9) x3_minus) (* (- 25) x2_plus) (* 25 x2_minus) ) (- 63) ) )
(assert (>= (+ (* 45 x9_plus) (* (- 45) x9_minus) (* 13 x6_plus) (* (- 13) x6_minus) (* (- 72) x5_plus) (* 72 x5_minus) (* (- 59) x4_plus) (* 59 x4_minus) (* (- 146) x3_plus) (* 146 x3_minus) (* (- 70) x2_plus) (* 70 x2_minus) ) 11 ) )
(assert (>= (+ (* 17 x9_plus) (* (- 17) x9_minus) (* 3 x8_plus) (* (- 3) x8_minus) (* (- 100) x6_plus) (* 100 x6_minus) (* (- 21) x4_plus) (* 21 x4_minus) (* (- 51) x3_plus) (* 51 x3_minus) (* (- 83) x1_plus) (* 83 x1_minus) ) 15 ) )
(assert (>= (+ (* 151 x9_plus) (* (- 151) x9_minus) (* (- 57) x8_plus) (* 57 x8_minus) (* 107 x5_plus) (* (- 107) x5_minus) (* 32 x4_plus) (* (- 32) x4_minus) (* (- 72) x3_plus) (* 72 x3_minus) ) 43 ) )
(assert (>= (+ (* 60 x8_plus) (* (- 60) x8_minus) (* (- 37) x6_plus) (* 37 x6_minus) (* (- 70) x4_plus) (* 70 x4_minus) (* (- 66) x0_plus) (* 66 x0_minus) ) 14 ) )
(check-sat)
(exit)