(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 x7_plus () Int) (declare-fun x7_minus () Int) (declare-fun x5_plus () Int) (declare-fun x5_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 x6_plus () Int) (declare-fun x6_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 (>= x5_plus 0)) (assert (>= x5_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 (>= x6_plus 0)) (assert (>= x6_minus 0)) (assert (<= (+ (* 5 x9_plus) (* (- 5) x9_minus) (* (- 12) x8_plus) (* 12 x8_minus) (* 77 x7_plus) (* (- 77) x7_minus) (* 65 x5_plus) (* (- 65) x5_minus) (* (- 12) x4_plus) (* 12 x4_minus) (* 24 x3_plus) (* (- 24) x3_minus) (* 113 x2_plus) (* (- 113) x2_minus) (* 42 x1_plus) (* (- 42) x1_minus) ) 37 ) ) (assert (<= (+ (* 39 x9_plus) (* (- 39) x9_minus) (* 13 x8_plus) (* (- 13) x8_minus) (* 11 x5_plus) (* (- 11) x5_minus) (* 77 x4_plus) (* (- 77) x4_minus) (* 77 x3_plus) (* (- 77) x3_minus) (* 6 x2_plus) (* (- 6) x2_minus) (* 71 x1_plus) (* (- 71) x1_minus) (* 162 x0_plus) (* (- 162) x0_minus) ) 47 ) ) (assert (<= (+ (* 70 x9_plus) (* (- 70) x9_minus) (* (- 31) x8_plus) (* 31 x8_minus) (* 88 x7_plus) (* (- 88) x7_minus) (* 18 x6_plus) (* (- 18) x6_minus) (* (- 117) x4_plus) (* 117 x4_minus) (* (- 42) x3_plus) (* 42 x3_minus) (* (- 66) x1_plus) (* 66 x1_minus) ) 68 ) ) (assert (<= (+ (* 42 x9_plus) (* (- 42) x9_minus) (* 52 x7_plus) (* (- 52) x7_minus) (* 28 x6_plus) (* (- 28) x6_minus) (* 37 x4_plus) (* (- 37) x4_minus) (* 24 x3_plus) (* (- 24) x3_minus) (* 44 x2_plus) (* (- 44) x2_minus) (* (- 22) x1_plus) (* 22 x1_minus) ) 28 ) ) (assert (<= (+ (* 44 x7_plus) (* (- 44) x7_minus) (* (- 87) x6_plus) (* 87 x6_minus) (* (- 81) x5_plus) (* 81 x5_minus) (* 81 x4_plus) (* (- 81) x4_minus) (* (- 7) x2_plus) (* 7 x2_minus) (* (- 85) x1_plus) (* 85 x1_minus) (* (- 53) x0_plus) (* 53 x0_minus) ) 31 ) ) (assert (<= (+ (* 6 x8_plus) (* (- 6) x8_minus) (* 35 x7_plus) (* (- 35) x7_minus) (* 64 x6_plus) (* (- 64) x6_minus) (* 119 x5_plus) (* (- 119) x5_minus) (* 77 x3_plus) (* (- 77) x3_minus) (* (- 85) x2_plus) (* 85 x2_minus) (* (- 42) x0_plus) (* 42 x0_minus) ) (- 85) ) ) (assert (<= (+ (* 90 x9_plus) (* (- 90) x9_minus) (* 69 x8_plus) (* (- 69) x8_minus) (* 49 x7_plus) (* (- 49) x7_minus) (* (- 69) x5_plus) (* 69 x5_minus) (* 73 x4_plus) (* (- 73) x4_minus) (* (- 23) x2_plus) (* 23 x2_minus) ) 42 ) ) (assert (<= (+ (* 71 x9_plus) (* (- 71) x9_minus) (* 48 x8_plus) (* (- 48) x8_minus) (* (- 43) x6_plus) (* 43 x6_minus) (* (- 125) x4_plus) (* 125 x4_minus) (* (- 60) x2_plus) (* 60 x2_minus) (* 38 x0_plus) (* (- 38) x0_minus) ) (- 6) ) ) (assert (<= (+ (* 8 x9_plus) (* (- 8) x9_minus) (* 72 x8_plus) (* (- 72) x8_minus) (* (- 29) x7_plus) (* 29 x7_minus) (* 67 x6_plus) (* (- 67) x6_minus) (* 83 x4_plus) (* (- 83) x4_minus) (* 77 x2_plus) (* (- 77) x2_minus) ) 20 ) ) (assert (<= (+ (* 79 x9_plus) (* (- 79) x9_minus) (* 34 x8_plus) (* (- 34) x8_minus) (* 107 x6_plus) (* (- 107) x6_minus) (* 31 x5_plus) (* (- 31) x5_minus) (* 33 x3_plus) (* (- 33) x3_minus) (* 16 x2_plus) (* (- 16) x2_minus) ) (- 87) ) ) (assert (<= (+ (* 56 x9_plus) (* (- 56) x9_minus) (* (- 68) x7_plus) (* 68 x7_minus) (* 103 x6_plus) (* (- 103) x6_minus) (* 56 x4_plus) (* (- 56) x4_minus) (* (- 54) x2_plus) (* 54 x2_minus) ) (- 54) ) ) (assert (<= (+ (* 9 x8_plus) (* (- 9) x8_minus) (* 62 x7_plus) (* (- 62) x7_minus) (* (- 108) x5_plus) (* 108 x5_minus) (* 134 x3_plus) (* (- 134) x3_minus) (* 79 x2_plus) (* (- 79) x2_minus) ) 85 ) ) (assert (<= (+ (* 70 x7_plus) (* (- 70) x7_minus) (* 14 x6_plus) (* (- 14) x6_minus) (* 3 x5_plus) (* (- 3) x5_minus) (* 25 x1_plus) (* (- 25) x1_minus) (* (- 26) x0_plus) (* 26 x0_minus) ) 72 ) ) (assert (>= (+ (* 77 x9_plus) (* (- 77) x9_minus) (* 29 x8_plus) (* (- 29) x8_minus) (* 24 x7_plus) (* (- 24) x7_minus) (* (- 16) x6_plus) (* 16 x6_minus) (* 26 x5_plus) (* (- 26) x5_minus) (* 39 x4_plus) (* (- 39) x4_minus) (* (- 63) x3_plus) (* 63 x3_minus) (* (- 25) x1_plus) (* 25 x1_minus) ) (- 69) ) ) (assert (>= (+ (* 9 x9_plus) (* (- 9) x9_minus) (* (- 19) x8_plus) (* 19 x8_minus) (* (- 63) x7_plus) (* 63 x7_minus) (* (- 74) x4_plus) (* 74 x4_minus) (* (- 61) x2_plus) (* 61 x2_minus) (* (- 16) x1_plus) (* 16 x1_minus) (* 77 x0_plus) (* (- 77) x0_minus) ) (- 38) ) ) (assert (>= (+ (* 66 x8_plus) (* (- 66) x8_minus) (* 11 x6_plus) (* (- 11) x6_minus) (* 74 x4_plus) (* (- 74) x4_minus) (* (- 42) x3_plus) (* 42 x3_minus) (* (- 83) x1_plus) (* 83 x1_minus) (* (- 135) x0_plus) (* 135 x0_minus) ) 22 ) ) (assert (>= (+ (* 57 x9_plus) (* (- 57) x9_minus) (* (- 136) x8_plus) (* 136 x8_minus) (* 131 x4_plus) (* (- 131) x4_minus) (* 34 x3_plus) (* (- 34) x3_minus) (* (- 11) x1_plus) (* 11 x1_minus) (* (- 72) x0_plus) (* 72 x0_minus) ) 43 ) ) (assert (>= (+ (* 9 x9_plus) (* (- 9) x9_minus) (* (- 83) x7_plus) (* 83 x7_minus) (* (- 88) x6_plus) (* 88 x6_minus) (* 105 x4_plus) (* (- 105) x4_minus) (* (- 109) x1_plus) (* 109 x1_minus) (* (- 84) x0_plus) (* 84 x0_minus) ) (- 54) ) ) (assert (>= (+ (* 63 x8_plus) (* (- 63) x8_minus) (* (- 2) x7_plus) (* 2 x7_minus) (* (- 2) x6_plus) (* 2 x6_minus) (* (- 52) x5_plus) (* 52 x5_minus) (* 77 x4_plus) (* (- 77) x4_minus) (* (- 31) x3_plus) (* 31 x3_minus) ) (- 41) ) ) (assert (>= (+ (* 63 x9_plus) (* (- 63) x9_minus) (* (- 1) x6_plus) x6_minus (* 83 x5_plus) (* (- 83) x5_minus) (* 27 x2_plus) (* (- 27) x2_minus) (* (- 35) x0_plus) (* 35 x0_minus) ) 83 ) ) (check-sat) (exit)