(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 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 x7_plus () Int)
(declare-fun x7_minus () Int)
(declare-fun x3_plus () Int)
(declare-fun x3_minus () Int)
(assert (>= x9_plus 0))
(assert (>= x9_minus 0))
(assert (>= x8_plus 0))
(assert (>= x8_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 (>= x7_plus 0))
(assert (>= x7_minus 0))
(assert (>= x3_plus 0))
(assert (>= x3_minus 0))
(assert (<= (+ (* 20 x9_plus) (* (- 20) x9_minus) (* (- 44) x8_plus) (* 44 x8_minus) (* (- 16) x6_plus) (* 16 x6_minus) (* 11 x5_plus) (* (- 11) x5_minus) (* 21 x4_plus) (* (- 21) x4_minus) (* 99 x2_plus) (* (- 99) x2_minus) (* (- 126) x1_plus) (* 126 x1_minus) (* (- 49) x0_plus) (* 49 x0_minus) ) 57 ) )
(assert (<= (+ (* 6 x8_plus) (* (- 6) x8_minus) (* 100 x7_plus) (* (- 100) x7_minus) (* 38 x6_plus) (* (- 38) x6_minus) (* (- 16) x5_plus) (* 16 x5_minus) (* 23 x4_plus) (* (- 23) x4_minus) (* 42 x3_plus) (* (- 42) x3_minus) (* 63 x2_plus) (* (- 63) x2_minus) (* 58 x0_plus) (* (- 58) x0_minus) ) (- 37) ) )
(assert (<= (+ (* 34 x9_plus) (* (- 34) x9_minus) (* (- 27) x8_plus) (* 27 x8_minus) (* 9 x7_plus) (* (- 9) x7_minus) (* 6 x5_plus) (* (- 6) x5_minus) (* 14 x3_plus) (* (- 14) x3_minus) (* 64 x2_plus) (* (- 64) x2_minus) (* (- 58) x1_plus) (* 58 x1_minus) ) 15 ) )
(assert (<= (+ (* 14 x9_plus) (* (- 14) x9_minus) (* 38 x6_plus) (* (- 38) x6_minus) (* (- 8) x5_plus) (* 8 x5_minus) (* 26 x4_plus) (* (- 26) x4_minus) (* (- 39) x2_plus) (* 39 x2_minus) (* 19 x1_plus) (* (- 19) x1_minus) (* 5 x0_plus) (* (- 5) x0_minus) ) (- 35) ) )
(assert (<= (+ (* 59 x8_plus) (* (- 59) x8_minus) (* (- 39) x7_plus) (* 39 x7_minus) (* (- 26) x5_plus) (* 26 x5_minus) (* (- 59) x3_plus) (* 59 x3_minus) (* (- 14) x2_plus) (* 14 x2_minus) (* 18 x1_plus) (* (- 18) x1_minus) (* 14 x0_plus) (* (- 14) x0_minus) ) (- 15) ) )
(assert (<= (+ (* 64 x9_plus) (* (- 64) x9_minus) (* (- 13) x7_plus) (* 13 x7_minus) (* 103 x6_plus) (* (- 103) x6_minus) (* 50 x4_plus) (* (- 50) x4_minus) (* 60 x2_plus) (* (- 60) x2_minus) (* 9 x0_plus) (* (- 9) x0_minus) ) 58 ) )
(assert (<= (+ (* 13 x9_plus) (* (- 13) x9_minus) (* 41 x8_plus) (* (- 41) x8_minus) (* 24 x5_plus) (* (- 24) x5_minus) (* (- 28) x4_plus) (* 28 x4_minus) (* (- 64) x3_plus) (* 64 x3_minus) (* (- 66) x2_plus) (* 66 x2_minus) ) 38 ) )
(assert (<= (+ (* 112 x9_plus) (* (- 112) x9_minus) (* (- 60) x6_plus) (* 60 x6_minus) (* 22 x4_plus) (* (- 22) x4_minus) (* (- 42) x3_plus) (* 42 x3_minus) (* (- 12) x2_plus) (* 12 x2_minus) (* (- 25) x1_plus) (* 25 x1_minus) ) 50 ) )
(assert (<= (+ (* 31 x8_plus) (* (- 31) x8_minus) (* 27 x5_plus) (* (- 27) x5_minus) (* (- 9) x4_plus) (* 9 x4_minus) (* 13 x3_plus) (* (- 13) x3_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* (- 20) x1_plus) (* 20 x1_minus) ) 17 ) )
(assert (<= (+ (* 28 x9_plus) (* (- 28) x9_minus) (* 58 x8_plus) (* (- 58) x8_minus) (* 3 x7_plus) (* (- 3) x7_minus) (* 34 x2_plus) (* (- 34) x2_minus) (* (- 28) x1_plus) (* 28 x1_minus) (* 22 x0_plus) (* (- 22) x0_minus) ) 53 ) )
(assert (<= (+ (* 49 x7_plus) (* (- 49) x7_minus) (* 41 x6_plus) (* (- 41) x6_minus) (* (- 73) x5_plus) (* 73 x5_minus) (* 7 x3_plus) (* (- 7) x3_minus) (* (- 36) x2_plus) (* 36 x2_minus) (* (- 3) x0_plus) (* 3 x0_minus) ) 36 ) )
(assert (<= (+ (* 22 x8_plus) (* (- 22) x8_minus) (* 9 x7_plus) (* (- 9) x7_minus) (* 45 x5_plus) (* (- 45) x5_minus) (* 12 x4_plus) (* (- 12) x4_minus) (* 23 x2_plus) (* (- 23) x2_minus) (* 58 x0_plus) (* (- 58) x0_minus) ) (- 46) ) )
(assert (<= (+ (* 120 x8_plus) (* (- 120) x8_minus) (* (- 65) x7_plus) (* 65 x7_minus) (* 57 x6_plus) (* (- 57) x6_minus) (* (- 34) x4_plus) (* 34 x4_minus) (* 51 x0_plus) (* (- 51) x0_minus) ) 11 ) )
(assert (<= (+ (* 80 x8_plus) (* (- 80) x8_minus) (* 58 x7_plus) (* (- 58) x7_minus) (* 52 x6_plus) (* (- 52) x6_minus) (* (- 50) x4_plus) (* 50 x4_minus) (* 21 x2_plus) (* (- 21) x2_minus) ) (- 38) ) )
(assert (<= (+ (* 6 x6_plus) (* (- 6) x6_minus) (* 29 x4_plus) (* (- 29) x4_minus) (* (- 10) x3_plus) (* 10 x3_minus) (* 65 x1_plus) (* (- 65) x1_minus) (* (- 66) x0_plus) (* 66 x0_minus) ) (- 38) ) )
(assert (>= (+ (* 11 x8_plus) (* (- 11) x8_minus) (* (- 56) x7_plus) (* 56 x7_minus) (* (- 79) x6_plus) (* 79 x6_minus) (* (- 15) x4_plus) (* 15 x4_minus) (* 44 x3_plus) (* (- 44) x3_minus) (* 63 x2_plus) (* (- 63) x2_minus) (* (- 23) x1_plus) (* 23 x1_minus) ) (- 46) ) )
(assert (>= (+ (* 63 x9_plus) (* (- 63) x9_minus) (* 56 x7_plus) (* (- 56) x7_minus) (* 40 x6_plus) (* (- 40) x6_minus) (* (- 35) x5_plus) (* 35 x5_minus) (* 50 x2_plus) (* (- 50) x2_minus) (* 78 x1_plus) (* (- 78) x1_minus) (* 114 x0_plus) (* (- 114) x0_minus) ) (- 26) ) )
(assert (>= (+ (* 127 x9_plus) (* (- 127) x9_minus) (* 47 x7_plus) (* (- 47) x7_minus) (* (- 25) x6_plus) (* 25 x6_minus) x5_plus (* (- 1) x5_minus) (* (- 55) x2_plus) (* 55 x2_minus) (* (- 55) x1_plus) (* 55 x1_minus) (* 71 x0_plus) (* (- 71) x0_minus) ) (- 24) ) )
(assert (>= (+ (* 62 x9_plus) (* (- 62) x9_minus) (* (- 19) x8_plus) (* 19 x8_minus) (* (- 45) x7_plus) (* 45 x7_minus) (* 30 x4_plus) (* (- 30) x4_minus) (* 72 x3_plus) (* (- 72) x3_minus) (* 6 x2_plus) (* (- 6) x2_minus) ) 39 ) )
(assert (>= (+ (* 137 x7_plus) (* (- 137) x7_minus) (* 16 x6_plus) (* (- 16) x6_minus) (* 53 x5_plus) (* (- 53) x5_minus) (* (- 66) x2_plus) (* 66 x2_minus) (* (- 22) x0_plus) (* 22 x0_minus) ) (- 20) ) )
(check-sat)
(exit)