(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 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 x0_plus () Int) (declare-fun x0_minus () Int) (declare-fun x9_plus () Int) (declare-fun x9_minus () Int) (declare-fun x5_plus () Int) (declare-fun x5_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 (>= 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 (>= x0_plus 0)) (assert (>= x0_minus 0)) (assert (>= x9_plus 0)) (assert (>= x9_minus 0)) (assert (>= x5_plus 0)) (assert (>= x5_minus 0)) (assert (<= (+ (* 43 x8_plus) (* (- 43) x8_minus) (* 88 x7_plus) (* (- 88) x7_minus) (* 58 x6_plus) (* (- 58) x6_minus) (* (- 66) x4_plus) (* 66 x4_minus) (* 148 x3_plus) (* (- 148) x3_minus) (* (- 89) x2_plus) (* 89 x2_minus) (* 97 x1_plus) (* (- 97) x1_minus) (* (- 39) x0_plus) (* 39 x0_minus) ) (- 34) ) ) (assert (<= (+ (* 165 x9_plus) (* (- 165) x9_minus) (* 37 x8_plus) (* (- 37) x8_minus) (* 5 x7_plus) (* (- 5) x7_minus) (* (- 2) x6_plus) (* 2 x6_minus) (* 49 x5_plus) (* (- 49) x5_minus) (* (- 56) x4_plus) (* 56 x4_minus) (* 71 x1_plus) (* (- 71) x1_minus) (* 20 x0_plus) (* (- 20) x0_minus) ) (- 17) ) ) (assert (<= (+ (* 41 x9_plus) (* (- 41) x9_minus) (* 74 x8_plus) (* (- 74) x8_minus) (* (- 52) x7_plus) (* 52 x7_minus) (* 40 x6_plus) (* (- 40) x6_minus) (* (- 38) x3_plus) (* 38 x3_minus) (* 28 x2_plus) (* (- 28) x2_minus) (* 64 x0_plus) (* (- 64) x0_minus) ) 69 ) ) (assert (<= (+ (* 65 x9_plus) (* (- 65) x9_minus) (* (- 95) x7_plus) (* 95 x7_minus) (* 53 x6_plus) (* (- 53) x6_minus) (* (- 128) x5_plus) (* 128 x5_minus) (* (- 84) x2_plus) (* 84 x2_minus) (* 46 x1_plus) (* (- 46) x1_minus) (* 7 x0_plus) (* (- 7) x0_minus) ) (- 81) ) ) (assert (<= (+ (* 91 x8_plus) (* (- 91) x8_minus) (* 90 x7_plus) (* (- 90) x7_minus) (* (- 73) x6_plus) (* 73 x6_minus) (* (- 179) x3_plus) (* 179 x3_minus) (* 43 x2_plus) (* (- 43) x2_minus) (* 34 x1_plus) (* (- 34) x1_minus) (* 37 x0_plus) (* (- 37) x0_minus) ) (- 42) ) ) (assert (<= (+ (* 62 x8_plus) (* (- 62) x8_minus) (* 52 x7_plus) (* (- 52) x7_minus) (* 35 x5_plus) (* (- 35) x5_minus) (* 123 x4_plus) (* (- 123) x4_minus) (* (- 10) x2_plus) (* 10 x2_minus) (* 48 x1_plus) (* (- 48) x1_minus) (* 86 x0_plus) (* (- 86) x0_minus) ) 55 ) ) (assert (<= (+ (* 27 x8_plus) (* (- 27) x8_minus) (* (- 143) x7_plus) (* 143 x7_minus) (* 28 x6_plus) (* (- 28) x6_minus) (* 27 x5_plus) (* (- 27) x5_minus) (* (- 28) x3_plus) (* 28 x3_minus) (* 111 x2_plus) (* (- 111) x2_minus) ) (- 59) ) ) (assert (<= (+ (* 19 x8_plus) (* (- 19) x8_minus) (* 56 x7_plus) (* (- 56) x7_minus) (* (- 29) x6_plus) (* 29 x6_minus) (* (- 24) x5_plus) (* 24 x5_minus) (* 88 x4_plus) (* (- 88) x4_minus) (* 90 x2_plus) (* (- 90) x2_minus) ) 84 ) ) (assert (<= (+ (* 46 x9_plus) (* (- 46) x9_minus) (* (- 143) x8_plus) (* 143 x8_minus) (* 31 x7_plus) (* (- 31) x7_minus) (* 48 x3_plus) (* (- 48) x3_minus) (* 34 x1_plus) (* (- 34) x1_minus) (* 2 x0_plus) (* (- 2) x0_minus) ) (- 9) ) ) (assert (<= (+ (* 91 x9_plus) (* (- 91) x9_minus) (* 26 x7_plus) (* (- 26) x7_minus) (* (- 139) x5_plus) (* 139 x5_minus) (* (- 50) x4_plus) (* 50 x4_minus) (* 24 x2_plus) (* (- 24) x2_minus) (* (- 57) x1_plus) (* 57 x1_minus) ) (- 56) ) ) (assert (<= (+ (* 18 x9_plus) (* (- 18) x9_minus) (* 123 x8_plus) (* (- 123) x8_minus) (* 56 x7_plus) (* (- 56) x7_minus) (* (- 56) x4_plus) (* 56 x4_minus) (* (- 106) x2_plus) (* 106 x2_minus) (* 23 x0_plus) (* (- 23) x0_minus) ) 39 ) ) (assert (<= (+ (* 157 x9_plus) (* (- 157) x9_minus) (* 7 x7_plus) (* (- 7) x7_minus) (* (- 14) x6_plus) (* 14 x6_minus) (* (- 14) x3_plus) (* 14 x3_minus) (* (- 41) x2_plus) (* 41 x2_minus) (* 80 x0_plus) (* (- 80) x0_minus) ) 67 ) ) (assert (<= (+ (* 92 x9_plus) (* (- 92) x9_minus) (* 288 x8_plus) (* (- 288) x8_minus) (* (- 32) x6_plus) (* 32 x6_minus) (* (- 35) x4_plus) (* 35 x4_minus) (* (- 60) x3_plus) (* 60 x3_minus) ) (- 55) ) ) (assert (>= (+ (* 58 x9_plus) (* (- 58) x9_minus) (* 43 x8_plus) (* (- 43) x8_minus) (* 23 x7_plus) (* (- 23) x7_minus) (* (- 36) x6_plus) (* 36 x6_minus) (* (- 45) x3_plus) (* 45 x3_minus) (* (- 16) x2_plus) (* 16 x2_minus) (* 65 x1_plus) (* (- 65) x1_minus) ) 55 ) ) (assert (>= (+ (* 31 x7_plus) (* (- 31) x7_minus) (* 18 x6_plus) (* (- 18) x6_minus) (* 56 x5_plus) (* (- 56) x5_minus) (* (- 168) x3_plus) (* 168 x3_minus) (* (- 8) x2_plus) (* 8 x2_minus) (* (- 85) x1_plus) (* 85 x1_minus) (* (- 39) x0_plus) (* 39 x0_minus) ) (- 88) ) ) (assert (>= (+ (* 94 x9_plus) (* (- 94) x9_minus) (* 48 x7_plus) (* (- 48) x7_minus) (* (- 26) x5_plus) (* 26 x5_minus) (* 23 x4_plus) (* (- 23) x4_minus) (* 15 x2_plus) (* (- 15) x2_minus) (* (- 79) x1_plus) (* 79 x1_minus) (* (- 63) x0_plus) (* 63 x0_minus) ) (- 52) ) ) (assert (>= (+ (* 41 x8_plus) (* (- 41) x8_minus) (* (- 4) x7_plus) (* 4 x7_minus) (* (- 63) x5_plus) (* 63 x5_minus) (* 59 x4_plus) (* (- 59) x4_minus) (* 117 x3_plus) (* (- 117) x3_minus) (* (- 58) x2_plus) (* 58 x2_minus) (* 34 x1_plus) (* (- 34) x1_minus) ) 74 ) ) (assert (>= (+ (* 49 x9_plus) (* (- 49) x9_minus) (* 62 x8_plus) (* (- 62) x8_minus) (* (- 74) x6_plus) (* 74 x6_minus) (* 71 x3_plus) (* (- 71) x3_minus) (* (- 51) x2_plus) (* 51 x2_minus) (* 76 x0_plus) (* (- 76) x0_minus) ) (- 71) ) ) (assert (>= (+ (* 40 x9_plus) (* (- 40) x9_minus) (* (- 26) x8_plus) (* 26 x8_minus) (* (- 73) x7_plus) (* 73 x7_minus) (* 86 x6_plus) (* (- 86) x6_minus) (* 38 x5_plus) (* (- 38) x5_minus) (* 48 x4_plus) (* (- 48) x4_minus) ) (- 63) ) ) (assert (>= (+ (* 28 x8_plus) (* (- 28) x8_minus) (* (- 58) x6_plus) (* 58 x6_minus) (* (- 79) x5_plus) (* 79 x5_minus) (* (- 81) x4_plus) (* 81 x4_minus) (* (- 76) x1_plus) (* 76 x1_minus) (* (- 9) x0_plus) (* 9 x0_minus) ) (- 30) ) ) (check-sat) (exit)