(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 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 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 x9_plus () Int)
(declare-fun x9_minus () Int)
(declare-fun x3_plus () Int)
(declare-fun x3_minus () Int)
(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 (>= 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 (>= x9_plus 0))
(assert (>= x9_minus 0))
(assert (>= x3_plus 0))
(assert (>= x3_minus 0))
(assert (<= (+ (* 5 x8_plus) (* (- 5) x8_minus) (* (- 15) x7_plus) (* 15 x7_minus) (* 16 x6_plus) (* (- 16) x6_minus) (* (- 65) x5_plus) (* 65 x5_minus) (* 41 x4_plus) (* (- 41) x4_minus) (* (- 41) x2_plus) (* 41 x2_minus) (* 79 x1_plus) (* (- 79) x1_minus) (* (- 94) x0_plus) (* 94 x0_minus) ) (- 69) ) )
(assert (<= (+ (* 74 x9_plus) (* (- 74) x9_minus) (* (- 44) x8_plus) (* 44 x8_minus) (* 31 x7_plus) (* (- 31) x7_minus) (* 108 x6_plus) (* (- 108) x6_minus) (* (- 75) x5_plus) (* 75 x5_minus) (* (- 34) x4_plus) (* 34 x4_minus) (* 17 x1_plus) (* (- 17) x1_minus) (* 72 x0_plus) (* (- 72) x0_minus) ) (- 75) ) )
(assert (<= (+ (* 72 x9_plus) (* (- 72) x9_minus) (* (- 12) x8_plus) (* 12 x8_minus) (* (- 32) x7_plus) (* 32 x7_minus) (* (- 22) x5_plus) (* 22 x5_minus) (* (- 78) x4_plus) (* 78 x4_minus) (* 57 x1_plus) (* (- 57) x1_minus) (* 32 x0_plus) (* (- 32) x0_minus) ) (- 30) ) )
(assert (<= (+ (* 39 x9_plus) (* (- 39) x9_minus) (* (- 66) x8_plus) (* 66 x8_minus) (* (- 37) x7_plus) (* 37 x7_minus) (* (- 49) x6_plus) (* 49 x6_minus) (* 54 x5_plus) (* (- 54) x5_minus) (* (- 62) x3_plus) (* 62 x3_minus) (* (- 12) x0_plus) (* 12 x0_minus) ) (- 66) ) )
(assert (<= (+ (* 43 x9_plus) (* (- 43) x9_minus) (* 3 x6_plus) (* (- 3) x6_minus) (* (- 5) x3_plus) (* 5 x3_minus) (* 66 x2_plus) (* (- 66) x2_minus) (* (- 145) x1_plus) (* 145 x1_minus) (* 85 x0_plus) (* (- 85) x0_minus) ) (- 36) ) )
(assert (<= (+ (* 64 x8_plus) (* (- 64) x8_minus) (* (- 19) x7_plus) (* 19 x7_minus) (* 16 x5_plus) (* (- 16) x5_minus) (* (- 40) x3_plus) (* 40 x3_minus) (* (- 17) x2_plus) (* 17 x2_minus) ) 28 ) )
(assert (>= (+ (* 62 x9_plus) (* (- 62) x9_minus) (* (- 38) x8_plus) (* 38 x8_minus) (* 68 x6_plus) (* (- 68) x6_minus) (* (- 86) x5_plus) (* 86 x5_minus) (* (- 3) x4_plus) (* 3 x4_minus) (* (- 59) x3_plus) (* 59 x3_minus) (* 69 x1_plus) (* (- 69) x1_minus) (* 30 x0_plus) (* (- 30) x0_minus) ) 3 ) )
(assert (>= (+ (* 20 x9_plus) (* (- 20) x9_minus) (* 12 x8_plus) (* (- 12) x8_minus) (* 29 x6_plus) (* (- 29) x6_minus) (* (- 95) x5_plus) (* 95 x5_minus) (* 4 x4_plus) (* (- 4) x4_minus) (* 58 x1_plus) (* (- 58) x1_minus) (* (- 26) x0_plus) (* 26 x0_minus) ) (- 17) ) )
(assert (>= (+ (* 72 x9_plus) (* (- 72) x9_minus) (* 31 x6_plus) (* (- 31) x6_minus) (* (- 46) x5_plus) (* 46 x5_minus) (* (- 69) x4_plus) (* 69 x4_minus) (* (- 74) x3_plus) (* 74 x3_minus) (* 46 x1_plus) (* (- 46) x1_minus) (* (- 111) x0_plus) (* 111 x0_minus) ) 52 ) )
(assert (>= (+ (* 28 x9_plus) (* (- 28) x9_minus) (* (- 51) x8_plus) (* 51 x8_minus) (* (- 160) x6_plus) (* 160 x6_minus) (* 27 x5_plus) (* (- 27) x5_minus) (* (- 24) x3_plus) (* 24 x3_minus) (* (- 32) x1_plus) (* 32 x1_minus) (* (- 8) x0_plus) (* 8 x0_minus) ) 23 ) )
(assert (>= (+ (* 52 x9_plus) (* (- 52) x9_minus) (* (- 52) x8_plus) (* 52 x8_minus) (* (- 15) x6_plus) (* 15 x6_minus) (* (- 130) x5_plus) (* 130 x5_minus) (* (- 45) x4_plus) (* 45 x4_minus) (* 82 x3_plus) (* (- 82) x3_minus) (* (- 95) x0_plus) (* 95 x0_minus) ) 66 ) )
(assert (>= (+ (* 15 x9_plus) (* (- 15) x9_minus) (* (- 16) x6_plus) (* 16 x6_minus) (* (- 118) x4_plus) (* 118 x4_minus) (* (- 85) x3_plus) (* 85 x3_minus) (* 7 x2_plus) (* (- 7) x2_minus) (* 66 x1_plus) (* (- 66) x1_minus) (* 65 x0_plus) (* (- 65) x0_minus) ) (- 38) ) )
(assert (>= (+ x8_plus (* (- 1) x8_minus) (* 70 x7_plus) (* (- 70) x7_minus) (* 35 x5_plus) (* (- 35) x5_minus) (* (- 64) x4_plus) (* 64 x4_minus) (* 47 x1_plus) (* (- 47) x1_minus) (* (- 54) x0_plus) (* 54 x0_minus) ) (- 3) ) )
(assert (>= (+ (* 55 x9_plus) (* (- 55) x9_minus) (* 19 x8_plus) (* (- 19) x8_minus) (* (- 4) x6_plus) (* 4 x6_minus) (* (- 50) x5_plus) (* 50 x5_minus) (* (- 94) x1_plus) (* 94 x1_minus) (* 41 x0_plus) (* (- 41) x0_minus) ) 41 ) )
(assert (>= (+ (* 49 x7_plus) (* (- 49) x7_minus) (* 41 x6_plus) (* (- 41) x6_minus) (* (- 64) x5_plus) (* 64 x5_minus) (* 3 x3_plus) (* (- 3) x3_minus) (* 14 x2_plus) (* (- 14) x2_minus) (* (- 38) x1_plus) (* 38 x1_minus) ) 18 ) )
(assert (>= (+ (* 25 x8_plus) (* (- 25) x8_minus) (* 47 x6_plus) (* (- 47) x6_minus) (* (- 68) x5_plus) (* 68 x5_minus) (* (- 65) x4_plus) (* 65 x4_minus) (* (- 34) x3_plus) (* 34 x3_minus) (* 70 x0_plus) (* (- 70) x0_minus) ) 2 ) )
(assert (>= (+ (* 34 x9_plus) (* (- 34) x9_minus) (* 129 x8_plus) (* (- 129) x8_minus) (* 55 x5_plus) (* (- 55) x5_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* (- 58) x1_plus) (* 58 x1_minus) (* 85 x0_plus) (* (- 85) x0_minus) ) 13 ) )
(assert (>= (+ (* 47 x8_plus) (* (- 47) x8_minus) (* (- 3) x7_plus) (* 3 x7_minus) (* 72 x6_plus) (* (- 72) x6_minus) (* 24 x2_plus) (* (- 24) x2_minus) (* 27 x0_plus) (* (- 27) x0_minus) ) (- 43) ) )
(assert (>= (+ (* 73 x9_plus) (* (- 73) x9_minus) (* 186 x4_plus) (* (- 186) x4_minus) (* (- 16) x3_plus) (* 16 x3_minus) (* (- 53) x2_plus) (* 53 x2_minus) (* (- 49) x0_plus) (* 49 x0_minus) ) 45 ) )
(assert (>= (+ (* 56 x8_plus) (* (- 56) x8_minus) (* 45 x7_plus) (* (- 45) x7_minus) (* 82 x6_plus) (* (- 82) x6_minus) (* 46 x2_plus) (* (- 46) x2_minus) (* (- 8) x1_plus) (* 8 x1_minus) ) (- 49) ) )
(check-sat)
(exit)