(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 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 (<= (+ (* 35 x9_plus) (* (- 35) x9_minus) (* 53 x8_plus) (* (- 53) x8_minus) (* 85 x7_plus) (* (- 85) x7_minus) (* 50 x6_plus) (* (- 50) x6_minus) (* 8 x5_plus) (* (- 8) x5_minus) (* (- 71) x3_plus) (* 71 x3_minus) (* 12 x2_plus) (* (- 12) x2_minus) (* (- 47) x1_plus) (* 47 x1_minus) (* 66 x0_plus) (* (- 66) x0_minus) ) (- 27) ) )
(assert (<= (+ (* 47 x8_plus) (* (- 47) x8_minus) (* (- 9) x7_plus) (* 9 x7_minus) (* 55 x6_plus) (* (- 55) x6_minus) (* (- 130) x5_plus) (* 130 x5_minus) (* (- 53) x4_plus) (* 53 x4_minus) (* 66 x3_plus) (* (- 66) x3_minus) (* (- 58) x1_plus) (* 58 x1_minus) (* 52 x0_plus) (* (- 52) x0_minus) ) (- 53) ) )
(assert (<= (+ (* 99 x7_plus) (* (- 99) x7_minus) (* (- 73) x6_plus) (* 73 x6_minus) (* 18 x5_plus) (* (- 18) x5_minus) (* (- 22) x4_plus) (* 22 x4_minus) (* (- 99) x3_plus) (* 99 x3_minus) (* (- 26) x2_plus) (* 26 x2_minus) (* 18 x1_plus) (* (- 18) x1_minus) (* (- 44) x0_plus) (* 44 x0_minus) ) (- 87) ) )
(assert (<= (+ (* 76 x8_plus) (* (- 76) x8_minus) (* (- 124) x7_plus) (* 124 x7_minus) (* 95 x6_plus) (* (- 95) x6_minus) (* (- 28) x5_plus) (* 28 x5_minus) (* (- 34) x4_plus) (* 34 x4_minus) (* (- 35) x3_plus) (* 35 x3_minus) (* (- 76) x2_plus) (* 76 x2_minus) x0_plus (* (- 1) x0_minus) ) (- 23) ) )
(assert (<= (+ (* 7 x9_plus) (* (- 7) x9_minus) (* 2 x8_plus) (* (- 2) x8_minus) (* 94 x5_plus) (* (- 94) x5_minus) (* 23 x3_plus) (* (- 23) x3_minus) (* 55 x2_plus) (* (- 55) x2_minus) (* 9 x1_plus) (* (- 9) x1_minus) (* 113 x0_plus) (* (- 113) x0_minus) ) 60 ) )
(assert (<= (+ (* 10 x9_plus) (* (- 10) x9_minus) (* 18 x8_plus) (* (- 18) x8_minus) (* (- 78) x7_plus) (* 78 x7_minus) (* 31 x6_plus) (* (- 31) x6_minus) (* 115 x4_plus) (* (- 115) x4_minus) (* 19 x1_plus) (* (- 19) x1_minus) (* 72 x0_plus) (* (- 72) x0_minus) ) (- 96) ) )
(assert (<= (+ (* 35 x7_plus) (* (- 35) x7_minus) (* 105 x6_plus) (* (- 105) x6_minus) (* (- 67) x5_plus) (* 67 x5_minus) (* (- 63) x4_plus) (* 63 x4_minus) (* (- 73) x3_plus) (* 73 x3_minus) (* 42 x1_plus) (* (- 42) x1_minus) (* (- 44) x0_plus) (* 44 x0_minus) ) (- 33) ) )
(assert (<= (+ (* 95 x9_plus) (* (- 95) x9_minus) (* 48 x7_plus) (* (- 48) x7_minus) (* 99 x6_plus) (* (- 99) x6_minus) (* 81 x5_plus) (* (- 81) x5_minus) (* 34 x4_plus) (* (- 34) x4_minus) (* (- 54) x2_plus) (* 54 x2_minus) (* 85 x0_plus) (* (- 85) x0_minus) ) (- 81) ) )
(assert (<= (+ (* 7 x9_plus) (* (- 7) x9_minus) (* (- 18) x7_plus) (* 18 x7_minus) (* 105 x6_plus) (* (- 105) x6_minus) (* 25 x5_plus) (* (- 25) x5_minus) (* (- 36) x4_plus) (* 36 x4_minus) (* (- 41) x3_plus) (* 41 x3_minus) (* 69 x1_plus) (* (- 69) x1_minus) ) (- 18) ) )
(assert (<= (+ (* 11 x8_plus) (* (- 11) x8_minus) (* (- 77) x7_plus) (* 77 x7_minus) (* (- 73) x6_plus) (* 73 x6_minus) (* (- 56) x5_plus) (* 56 x5_minus) (* 69 x4_plus) (* (- 69) x4_minus) (* 155 x2_plus) (* (- 155) x2_minus) (* (- 136) x0_plus) (* 136 x0_minus) ) 1 ) )
(assert (<= (+ (* 48 x9_plus) (* (- 48) x9_minus) (* 66 x8_plus) (* (- 66) x8_minus) (* 53 x7_plus) (* (- 53) x7_minus) (* 26 x3_plus) (* (- 26) x3_minus) (* (- 69) x2_plus) (* 69 x2_minus) (* (- 112) x1_plus) (* 112 x1_minus) ) (- 5) ) )
(assert (<= (+ (* 5 x9_plus) (* (- 5) x9_minus) (* 62 x8_plus) (* (- 62) x8_minus) (* 95 x7_plus) (* (- 95) x7_minus) (* (- 9) x4_plus) (* 9 x4_minus) (* 21 x1_plus) (* (- 21) x1_minus) (* 4 x0_plus) (* (- 4) x0_minus) ) 88 ) )
(assert (<= (+ (* 118 x6_plus) (* (- 118) x6_minus) (* 29 x5_plus) (* (- 29) x5_minus) (* (- 54) x4_plus) (* 54 x4_minus) (* (- 22) x3_plus) (* 22 x3_minus) (* 12 x1_plus) (* (- 12) x1_minus) (* (- 48) x0_plus) (* 48 x0_minus) ) 93 ) )
(assert (<= (+ (* 32 x9_plus) (* (- 32) x9_minus) (* 69 x6_plus) (* (- 69) x6_minus) (* (- 60) x5_plus) (* 60 x5_minus) (* (- 154) x3_plus) (* 154 x3_minus) x1_plus (* (- 1) x1_minus) ) 72 ) )
(assert (>= (+ (* 45 x9_plus) (* (- 45) x9_minus) (* 91 x8_plus) (* (- 91) x8_minus) (* 66 x6_plus) (* (- 66) x6_minus) (* 96 x5_plus) (* (- 96) x5_minus) (* 102 x3_plus) (* (- 102) x3_minus) (* (- 78) x2_plus) (* 78 x2_minus) (* (- 89) x1_plus) (* 89 x1_minus) (* (- 29) x0_plus) (* 29 x0_minus) ) 80 ) )
(assert (>= (+ (* 53 x9_plus) (* (- 53) x9_minus) (* 99 x8_plus) (* (- 99) x8_minus) (* 59 x7_plus) (* (- 59) x7_minus) (* 71 x4_plus) (* (- 71) x4_minus) (* (- 96) x3_plus) (* 96 x3_minus) (* 111 x2_plus) (* (- 111) x2_minus) (* (- 34) x1_plus) (* 34 x1_minus) ) 63 ) )
(assert (>= (+ (* 43 x9_plus) (* (- 43) x9_minus) (* 87 x7_plus) (* (- 87) x7_minus) (* (- 20) x5_plus) (* 20 x5_minus) (* 46 x4_plus) (* (- 46) x4_minus) (* 89 x1_plus) (* (- 89) x1_minus) (* (- 6) x0_plus) (* 6 x0_minus) ) (- 3) ) )
(assert (>= (+ (* 67 x8_plus) (* (- 67) x8_minus) (* 45 x7_plus) (* (- 45) x7_minus) (* 92 x5_plus) (* (- 92) x5_minus) (* (- 85) x3_plus) (* 85 x3_minus) (* (- 63) x2_plus) (* 63 x2_minus) (* (- 76) x1_plus) (* 76 x1_minus) ) 38 ) )
(assert (>= (+ (* 8 x9_plus) (* (- 8) x9_minus) (* (- 55) x7_plus) (* 55 x7_minus) (* 20 x5_plus) (* (- 20) x5_minus) (* (- 236) x4_plus) (* 236 x4_minus) (* (- 13) x3_plus) (* 13 x3_minus) (* (- 12) x0_plus) (* 12 x0_minus) ) (- 83) ) )
(assert (>= (+ (* 83 x9_plus) (* (- 83) x9_minus) (* (- 77) x7_plus) (* 77 x7_minus) (* (- 108) x6_plus) (* 108 x6_minus) (* (- 51) x4_plus) (* 51 x4_minus) (* (- 63) x2_plus) (* 63 x2_minus) (* (- 62) x1_plus) (* 62 x1_minus) ) 52 ) )
(check-sat)
(exit)