(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 (<= (+ (* 112 x8_plus) (* (- 112) x8_minus) (* 32 x7_plus) (* (- 32) x7_minus) (* 23 x6_plus) (* (- 23) x6_minus) (* 32 x5_plus) (* (- 32) x5_minus) (* 71 x4_plus) (* (- 71) x4_minus) (* (- 7) x2_plus) (* 7 x2_minus) (* (- 56) x1_plus) (* 56 x1_minus) (* (- 78) x0_plus) (* 78 x0_minus) ) 6 ) ) (assert (<= (+ (* 24 x9_plus) (* (- 24) x9_minus) (* 18 x8_plus) (* (- 18) x8_minus) (* (- 42) x7_plus) (* 42 x7_minus) (* (- 99) x6_plus) (* 99 x6_minus) (* (- 37) x4_plus) (* 37 x4_minus) (* 5 x3_plus) (* (- 5) x3_minus) (* (- 62) x2_plus) (* 62 x2_minus) (* (- 63) x0_plus) (* 63 x0_minus) ) (- 21) ) ) (assert (<= (+ (* 107 x9_plus) (* (- 107) x9_minus) (* 6 x7_plus) (* (- 6) x7_minus) (* (- 38) x6_plus) (* 38 x6_minus) (* 25 x4_plus) (* (- 25) x4_minus) (* 20 x3_plus) (* (- 20) x3_minus) (* 58 x1_plus) (* (- 58) x1_minus) (* (- 77) x0_plus) (* 77 x0_minus) ) (- 61) ) ) (assert (<= (+ (* 196 x9_plus) (* (- 196) x9_minus) (* (- 144) x7_plus) (* 144 x7_minus) (* (- 2) x6_plus) (* 2 x6_minus) (* 117 x5_plus) (* (- 117) x5_minus) (* (- 46) x4_plus) (* 46 x4_minus) (* 23 x1_plus) (* (- 23) x1_minus) ) (- 58) ) ) (assert (<= (+ (* 40 x8_plus) (* (- 40) x8_minus) (* (- 14) x6_plus) (* 14 x6_minus) (* (- 43) x5_plus) (* 43 x5_minus) (* (- 28) x2_plus) (* 28 x2_minus) (* 78 x1_plus) (* (- 78) x1_minus) (* (- 56) x0_plus) (* 56 x0_minus) ) 47 ) ) (assert (<= (+ (* 33 x9_plus) (* (- 33) x9_minus) (* (- 61) x8_plus) (* 61 x8_minus) (* (- 59) x7_plus) (* 59 x7_minus) (* 114 x5_plus) (* (- 114) x5_minus) (* 53 x4_plus) (* (- 53) x4_minus) (* 50 x3_plus) (* (- 50) x3_minus) ) (- 7) ) ) (assert (<= (+ (* 9 x7_plus) (* (- 9) x7_minus) (* (- 25) x6_plus) (* 25 x6_minus) (* 175 x5_plus) (* (- 175) x5_minus) (* 14 x4_plus) (* (- 14) x4_minus) (* (- 58) x3_plus) (* 58 x3_minus) (* (- 48) x0_plus) (* 48 x0_minus) ) 56 ) ) (assert (<= (+ (* 98 x8_plus) (* (- 98) x8_minus) (* 44 x7_plus) (* (- 44) x7_minus) (* 55 x5_plus) (* (- 55) x5_minus) (* 67 x4_plus) (* (- 67) x4_minus) (* (- 47) x2_plus) (* 47 x2_minus) (* (- 83) x0_plus) (* 83 x0_minus) ) 40 ) ) (assert (<= (+ (* 62 x8_plus) (* (- 62) x8_minus) (* (- 49) x7_plus) (* 49 x7_minus) (* 45 x6_plus) (* (- 45) x6_minus) (* 70 x3_plus) (* (- 70) x3_minus) (* 8 x2_plus) (* (- 8) x2_minus) (* (- 65) x1_plus) (* 65 x1_minus) ) (- 24) ) ) (assert (<= (+ (* 70 x8_plus) (* (- 70) x8_minus) (* 90 x7_plus) (* (- 90) x7_minus) (* 71 x3_plus) (* (- 71) x3_minus) (* (- 11) x2_plus) (* 11 x2_minus) (* (- 107) x1_plus) (* 107 x1_minus) (* (- 64) x0_plus) (* 64 x0_minus) ) 38 ) ) (assert (<= (+ (* 64 x9_plus) (* (- 64) x9_minus) (* (- 85) x7_plus) (* 85 x7_minus) (* 33 x6_plus) (* (- 33) x6_minus) (* 25 x3_plus) (* (- 25) x3_minus) (* 122 x2_plus) (* (- 122) x2_minus) ) (- 44) ) ) (assert (<= (+ (* 23 x9_plus) (* (- 23) x9_minus) (* 50 x7_plus) (* (- 50) x7_minus) (* 3 x4_plus) (* (- 3) x4_minus) (* 79 x3_plus) (* (- 79) x3_minus) (* (- 14) x1_plus) (* 14 x1_minus) ) 0 ) ) (assert (<= (+ (* 109 x8_plus) (* (- 109) x8_minus) (* (- 64) x7_plus) (* 64 x7_minus) (* 40 x5_plus) (* (- 40) x5_minus) (* 68 x2_plus) (* (- 68) x2_minus) (* 35 x0_plus) (* (- 35) x0_minus) ) (- 56) ) ) (assert (>= (+ (* 32 x9_plus) (* (- 32) x9_minus) (* (- 6) x8_plus) (* 6 x8_minus) (* (- 54) x6_plus) (* 54 x6_minus) (* 15 x5_plus) (* (- 15) x5_minus) x3_plus (* (- 1) x3_minus) (* (- 69) x2_plus) (* 69 x2_minus) (* 14 x1_plus) (* (- 14) x1_minus) (* (- 76) x0_plus) (* 76 x0_minus) ) 1 ) ) (assert (>= (+ (* 18 x8_plus) (* (- 18) x8_minus) (* (- 63) x6_plus) (* 63 x6_minus) (* (- 31) x4_plus) (* 31 x4_minus) (* (- 20) x3_plus) (* 20 x3_minus) (* (- 43) x2_plus) (* 43 x2_minus) (* (- 54) x1_plus) (* 54 x1_minus) x0_plus (* (- 1) x0_minus) ) 6 ) ) (assert (>= (+ (* 22 x9_plus) (* (- 22) x9_minus) (* (- 8) x7_plus) (* 8 x7_minus) (* (- 33) x5_plus) (* 33 x5_minus) (* (- 61) x4_plus) (* 61 x4_minus) (* 27 x3_plus) (* (- 27) x3_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* (- 61) x1_plus) (* 61 x1_minus) ) 6 ) ) (assert (>= (+ x9_plus (* (- 1) x9_minus) (* 55 x8_plus) (* (- 55) x8_minus) (* (- 6) x7_plus) (* 6 x7_minus) (* 22 x5_plus) (* (- 22) x5_minus) (* 78 x1_plus) (* (- 78) x1_minus) (* 77 x0_plus) (* (- 77) x0_minus) ) 29 ) ) (assert (>= (+ (* 53 x9_plus) (* (- 53) x9_minus) (* (- 56) x8_plus) (* 56 x8_minus) (* 74 x6_plus) (* (- 74) x6_minus) (* 12 x4_plus) (* (- 12) x4_minus) (* (- 63) x3_plus) (* 63 x3_minus) (* (- 71) x1_plus) (* 71 x1_minus) ) 57 ) ) (assert (>= (+ (* 68 x9_plus) (* (- 68) x9_minus) (* (- 35) x7_plus) (* 35 x7_minus) (* 31 x4_plus) (* (- 31) x4_minus) (* (- 125) x3_plus) (* 125 x3_minus) (* (- 34) x1_plus) (* 34 x1_minus) ) 48 ) ) (assert (>= (+ (* 53 x9_plus) (* (- 53) x9_minus) (* 135 x8_plus) (* (- 135) x8_minus) (* 46 x7_plus) (* (- 46) x7_minus) (* 22 x6_plus) (* (- 22) x6_minus) (* 162 x5_plus) (* (- 162) x5_minus) ) 37 ) ) (check-sat) (exit)