(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 x7_plus () Int)
(declare-fun x7_minus () Int)
(declare-fun x6_plus () Int)
(declare-fun x6_minus () Int)
(declare-fun x4_plus () Int)
(declare-fun x4_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 x5_plus () Int)
(declare-fun x5_minus () Int)
(declare-fun x0_plus () Int)
(declare-fun x0_minus () Int)
(declare-fun x8_plus () Int)
(declare-fun x8_minus () Int)
(assert (>= x9_plus 0))
(assert (>= x9_minus 0))
(assert (>= x7_plus 0))
(assert (>= x7_minus 0))
(assert (>= x6_plus 0))
(assert (>= x6_minus 0))
(assert (>= x4_plus 0))
(assert (>= x4_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 (>= x5_plus 0))
(assert (>= x5_minus 0))
(assert (>= x0_plus 0))
(assert (>= x0_minus 0))
(assert (>= x8_plus 0))
(assert (>= x8_minus 0))
(assert (<= (+ (* 21 x9_plus) (* (- 21) x9_minus) (* (- 21) x7_plus) (* 21 x7_minus) (* 49 x6_plus) (* (- 49) x6_minus) (* 55 x4_plus) (* (- 55) x4_minus) (* (- 25) x3_plus) (* 25 x3_minus) (* 11 x2_plus) (* (- 11) x2_minus) (* 16 x1_plus) (* (- 16) x1_minus) ) (- 16) ) )
(assert (<= (+ (* 19 x9_plus) (* (- 19) x9_minus) (* (- 69) x5_plus) (* 69 x5_minus) (* (- 15) x4_plus) (* 15 x4_minus) (* (- 66) x3_plus) (* 66 x3_minus) (* 43 x2_plus) (* (- 43) x2_minus) (* 18 x1_plus) (* (- 18) x1_minus) (* 24 x0_plus) (* (- 24) x0_minus) ) 51 ) )
(assert (<= (+ (* 17 x9_plus) (* (- 17) x9_minus) (* (- 4) x6_plus) (* 4 x6_minus) (* (- 23) x5_plus) (* 23 x5_minus) (* 74 x4_plus) (* (- 74) x4_minus) (* 60 x3_plus) (* (- 60) x3_minus) (* 39 x2_plus) (* (- 39) x2_minus) (* (- 42) x0_plus) (* 42 x0_minus) ) (- 34) ) )
(assert (<= (+ (* 28 x8_plus) (* (- 28) x8_minus) (* 68 x6_plus) (* (- 68) x6_minus) (* 41 x4_plus) (* (- 41) x4_minus) (* (- 105) x3_plus) (* 105 x3_minus) (* (- 25) x2_plus) (* 25 x2_minus) (* 92 x1_plus) (* (- 92) x1_minus) (* (- 20) x0_plus) (* 20 x0_minus) ) 22 ) )
(assert (<= (+ (* 68 x7_plus) (* (- 68) x7_minus) (* 82 x6_plus) (* (- 82) x6_minus) (* 18 x5_plus) (* (- 18) x5_minus) (* 62 x4_plus) (* (- 62) x4_minus) (* (- 45) x2_plus) (* 45 x2_minus) (* 16 x0_plus) (* (- 16) x0_minus) ) 47 ) )
(assert (<= (+ (* 37 x9_plus) (* (- 37) x9_minus) (* 99 x7_plus) (* (- 99) x7_minus) (* (- 44) x3_plus) (* 44 x3_minus) (* (- 24) x1_plus) (* 24 x1_minus) (* 39 x0_plus) (* (- 39) x0_minus) ) (- 47) ) )
(assert (>= (+ (* 66 x9_plus) (* (- 66) x9_minus) (* 65 x8_plus) (* (- 65) x8_minus) (* 36 x6_plus) (* (- 36) x6_minus) (* 5 x5_plus) (* (- 5) x5_minus) (* 97 x4_plus) (* (- 97) x4_minus) (* (- 1) x3_plus) x3_minus (* 5 x2_plus) (* (- 5) x2_minus) ) (- 40) ) )
(assert (>= (+ (* 44 x9_plus) (* (- 44) x9_minus) (* 57 x8_plus) (* (- 57) x8_minus) (* 4 x7_plus) (* (- 4) x7_minus) (* 61 x6_plus) (* (- 61) x6_minus) (* (- 69) x4_plus) (* 69 x4_minus) (* (- 59) x3_plus) (* 59 x3_minus) (* 80 x0_plus) (* (- 80) x0_minus) ) 44 ) )
(assert (>= (+ (* 24 x9_plus) (* (- 24) x9_minus) (* (- 57) x8_plus) (* 57 x8_minus) (* (- 8) x7_plus) (* 8 x7_minus) (* (- 62) x6_plus) (* 62 x6_minus) (* 64 x5_plus) (* (- 64) x5_minus) (* (- 47) x4_plus) (* 47 x4_minus) (* (- 9) x1_plus) (* 9 x1_minus) ) (- 68) ) )
(assert (>= (+ (* 14 x9_plus) (* (- 14) x9_minus) (* (- 59) x8_plus) (* 59 x8_minus) (* (- 31) x7_plus) (* 31 x7_minus) (* 37 x6_plus) (* (- 37) x6_minus) (* 75 x5_plus) (* (- 75) x5_minus) (* 8 x2_plus) (* (- 8) x2_minus) (* 26 x0_plus) (* (- 26) x0_minus) ) 44 ) )
(assert (>= (+ (* 16 x9_plus) (* (- 16) x9_minus) (* (- 56) x8_plus) (* 56 x8_minus) (* (- 65) x5_plus) (* 65 x5_minus) (* (- 19) x4_plus) (* 19 x4_minus) (* (- 65) x3_plus) (* 65 x3_minus) (* (- 21) x2_plus) (* 21 x2_minus) (* (- 17) x1_plus) (* 17 x1_minus) ) (- 57) ) )
(assert (>= (+ (* 41 x9_plus) (* (- 41) x9_minus) (* (- 30) x7_plus) (* 30 x7_minus) (* 47 x6_plus) (* (- 47) x6_minus) (* (- 77) x5_plus) (* 77 x5_minus) (* 67 x2_plus) (* (- 67) x2_minus) (* (- 42) x1_plus) (* 42 x1_minus) ) (- 22) ) )
(assert (>= (+ (* 24 x8_plus) (* (- 24) x8_minus) (* 24 x7_plus) (* (- 24) x7_minus) (* (- 92) x6_plus) (* 92 x6_minus) (* (- 51) x3_plus) (* 51 x3_minus) (* 52 x2_plus) (* (- 52) x2_minus) (* (- 55) x1_plus) (* 55 x1_minus) ) (- 5) ) )
(assert (>= (+ (* 45 x9_plus) (* (- 45) x9_minus) (* (- 66) x8_plus) (* 66 x8_minus) (* 11 x5_plus) (* (- 11) x5_minus) (* (- 46) x4_plus) (* 46 x4_minus) (* (- 83) x3_plus) (* 83 x3_minus) (* (- 44) x2_plus) (* 44 x2_minus) ) (- 41) ) )
(assert (>= (+ (* 37 x9_plus) (* (- 37) x9_minus) (* 14 x8_plus) (* (- 14) x8_minus) (* (- 23) x7_plus) (* 23 x7_minus) (* (- 64) x6_plus) (* 64 x6_minus) (* (- 183) x4_plus) (* 183 x4_minus) (* (- 52) x0_plus) (* 52 x0_minus) ) 40 ) )
(assert (>= (+ (* 57 x9_plus) (* (- 57) x9_minus) (* 36 x8_plus) (* (- 36) x8_minus) (* (- 64) x7_plus) (* 64 x7_minus) (* 23 x5_plus) (* (- 23) x5_minus) (* (- 34) x3_plus) (* 34 x3_minus) (* (- 16) x0_plus) (* 16 x0_minus) ) (- 67) ) )
(assert (>= (+ (* 120 x6_plus) (* (- 120) x6_minus) (* (- 11) x3_plus) (* 11 x3_minus) (* 5 x2_plus) (* (- 5) x2_minus) (* (- 67) x1_plus) (* 67 x1_minus) (* 10 x0_plus) (* (- 10) x0_minus) ) 52 ) )
(assert (>= (+ (* 35 x7_plus) (* (- 35) x7_minus) (* 24 x5_plus) (* (- 24) x5_minus) (* 47 x3_plus) (* (- 47) x3_minus) (* (- 173) x2_plus) (* 173 x2_minus) (* 16 x0_plus) (* (- 16) x0_minus) ) 53 ) )
(assert (>= (+ (* 43 x9_plus) (* (- 43) x9_minus) (* (- 8) x7_plus) (* 8 x7_minus) (* (- 20) x5_plus) (* 20 x5_minus) (* 59 x4_plus) (* (- 59) x4_minus) (* 74 x1_plus) (* (- 74) x1_minus) ) (- 53) ) )
(assert (>= (+ (* 68 x9_plus) (* (- 68) x9_minus) (* 19 x5_plus) (* (- 19) x5_minus) (* 77 x4_plus) (* (- 77) x4_minus) (* 32 x2_plus) (* (- 32) x2_minus) (* (- 69) x0_plus) (* 69 x0_minus) ) 52 ) )
(check-sat)
(exit)