(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 x9_plus () Int) (declare-fun x9_minus () Int) (declare-fun x3_plus () Int) (declare-fun x3_minus () Int) (declare-fun x0_plus () Int) (declare-fun x0_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 (>= x9_plus 0)) (assert (>= x9_minus 0)) (assert (>= x3_plus 0)) (assert (>= x3_minus 0)) (assert (>= x0_plus 0)) (assert (>= x0_minus 0)) (assert (<= (+ (* 57 x8_plus) (* (- 57) x8_minus) (* (- 58) x7_plus) (* 58 x7_minus) (* 60 x6_plus) (* (- 60) x6_minus) (* 85 x5_plus) (* (- 85) x5_minus) (* (- 2) x4_plus) (* 2 x4_minus) (* (- 58) x2_plus) (* 58 x2_minus) (* (- 32) x1_plus) (* 32 x1_minus) ) (- 52) ) ) (assert (<= (+ (* 33 x9_plus) (* (- 33) x9_minus) (* 49 x8_plus) (* (- 49) x8_minus) (* 19 x6_plus) (* (- 19) x6_minus) (* 63 x5_plus) (* (- 63) x5_minus) (* 30 x3_plus) (* (- 30) x3_minus) (* 22 x1_plus) (* (- 22) x1_minus) (* (- 45) x0_plus) (* 45 x0_minus) ) 30 ) ) (assert (<= (+ (* 45 x8_plus) (* (- 45) x8_minus) (* (- 43) x7_plus) (* 43 x7_minus) (* 24 x6_plus) (* (- 24) x6_minus) (* 83 x5_plus) (* (- 83) x5_minus) (* (- 50) x4_plus) (* 50 x4_minus) (* 56 x3_plus) (* (- 56) x3_minus) (* 25 x2_plus) (* (- 25) x2_minus) ) 47 ) ) (assert (<= (+ (* 36 x9_plus) (* (- 36) x9_minus) (* (- 41) x8_plus) (* 41 x8_minus) (* 97 x5_plus) (* (- 97) x5_minus) (* 8 x4_plus) (* (- 8) x4_minus) (* 84 x3_plus) (* (- 84) x3_minus) (* (- 10) x1_plus) (* 10 x1_minus) ) (- 2) ) ) (assert (<= (+ (* 21 x9_plus) (* (- 21) x9_minus) (* (- 27) x8_plus) (* 27 x8_minus) (* (- 10) x7_plus) (* 10 x7_minus) (* 57 x6_plus) (* (- 57) x6_minus) (* (- 5) x5_plus) (* 5 x5_minus) (* (- 69) x2_plus) (* 69 x2_minus) ) (- 16) ) ) (assert (<= (+ (* 12 x7_plus) (* (- 12) x7_minus) (* 19 x6_plus) (* (- 19) x6_minus) (* 5 x5_plus) (* (- 5) x5_minus) (* 50 x3_plus) (* (- 50) x3_minus) (* 47 x1_plus) (* (- 47) x1_minus) (* (- 42) x0_plus) (* 42 x0_minus) ) 39 ) ) (assert (<= (+ (* 62 x9_plus) (* (- 62) x9_minus) (* 35 x6_plus) (* (- 35) x6_minus) (* (- 14) x5_plus) (* 14 x5_minus) (* (- 14) x3_plus) (* 14 x3_minus) (* 14 x1_plus) (* (- 14) x1_minus) (* (- 42) x0_plus) (* 42 x0_minus) ) 16 ) ) (assert (<= (+ (* 35 x5_plus) (* (- 35) x5_minus) (* 24 x4_plus) (* (- 24) x4_minus) (* 67 x3_plus) (* (- 67) x3_minus) (* (- 3) x1_plus) (* 3 x1_minus) (* 11 x0_plus) (* (- 11) x0_minus) ) 23 ) ) (assert (<= (+ (* 9 x9_plus) (* (- 9) x9_minus) (* 45 x6_plus) (* (- 45) x6_minus) (* (- 94) x3_plus) (* 94 x3_minus) (* (- 27) x2_plus) (* 27 x2_minus) (* (- 42) x0_plus) (* 42 x0_minus) ) 53 ) ) (assert (<= (+ (* 15 x9_plus) (* (- 15) x9_minus) (* 7 x8_plus) (* (- 7) x8_minus) (* 39 x5_plus) (* (- 39) x5_minus) (* 50 x4_plus) (* (- 50) x4_minus) (* 40 x3_plus) (* (- 40) x3_minus) ) (- 25) ) ) (assert (>= (+ (* 53 x9_plus) (* (- 53) x9_minus) (* (- 23) x8_plus) (* 23 x8_minus) (* 36 x6_plus) (* (- 36) x6_minus) (* (- 30) x5_plus) (* 30 x5_minus) (* (- 20) x3_plus) (* 20 x3_minus) (* (- 45) x2_plus) (* 45 x2_minus) (* (- 22) x0_plus) (* 22 x0_minus) ) 18 ) ) (assert (>= (+ (* 12 x9_plus) (* (- 12) x9_minus) (* 18 x8_plus) (* (- 18) x8_minus) (* 60 x7_plus) (* (- 60) x7_minus) (* (- 58) x5_plus) (* 58 x5_minus) (* (- 46) x4_plus) (* 46 x4_minus) (* (- 57) x2_plus) (* 57 x2_minus) (* (- 47) x0_plus) (* 47 x0_minus) ) 49 ) ) (assert (>= (+ (* 61 x9_plus) (* (- 61) x9_minus) (* (- 12) x7_plus) (* 12 x7_minus) (* 14 x6_plus) (* (- 14) x6_minus) (* 10 x5_plus) (* (- 10) x5_minus) (* (- 30) x4_plus) (* 30 x4_minus) (* (- 39) x2_plus) (* 39 x2_minus) (* 9 x0_plus) (* (- 9) x0_minus) ) 13 ) ) (assert (>= (+ (* 42 x9_plus) (* (- 42) x9_minus) (* 29 x8_plus) (* (- 29) x8_minus) (* (- 36) x5_plus) (* 36 x5_minus) (* (- 17) x2_plus) (* 17 x2_minus) (* (- 27) x1_plus) (* 27 x1_minus) (* 50 x0_plus) (* (- 50) x0_minus) ) 31 ) ) (assert (>= (+ (* 30 x9_plus) (* (- 30) x9_minus) (* 21 x8_plus) (* (- 21) x8_minus) (* (- 52) x6_plus) (* 52 x6_minus) (* (- 14) x4_plus) (* 14 x4_minus) (* 54 x3_plus) (* (- 54) x3_minus) (* (- 63) x0_plus) (* 63 x0_minus) ) 1 ) ) (assert (>= (+ (* 4 x9_plus) (* (- 4) x9_minus) (* (- 52) x8_plus) (* 52 x8_minus) (* 77 x7_plus) (* (- 77) x7_minus) (* (- 5) x6_plus) (* 5 x6_minus) (* 57 x5_plus) (* (- 57) x5_minus) (* 30 x4_plus) (* (- 30) x4_minus) ) (- 45) ) ) (assert (>= (+ (* 34 x9_plus) (* (- 34) x9_minus) (* (- 98) x8_plus) (* 98 x8_minus) (* 7 x6_plus) (* (- 7) x6_minus) (* (- 61) x5_plus) (* 61 x5_minus) (* (- 9) x2_plus) (* 9 x2_minus) (* (- 82) x1_plus) (* 82 x1_minus) ) (- 43) ) ) (assert (>= (+ (* 7 x9_plus) (* (- 7) x9_minus) x8_plus (* (- 1) x8_minus) (* 14 x7_plus) (* (- 14) x7_minus) (* 28 x3_plus) (* (- 28) x3_minus) (* (- 7) x1_plus) (* 7 x1_minus) ) 4 ) ) (assert (>= (+ (* 90 x8_plus) (* (- 90) x8_minus) (* (- 38) x7_plus) (* 38 x7_minus) x4_plus (* (- 1) x4_minus) (* (- 45) x3_plus) (* 45 x3_minus) (* (- 11) x2_plus) (* 11 x2_minus) ) (- 55) ) ) (assert (>= (+ (* 53 x9_plus) (* (- 53) x9_minus) (* (- 62) x8_plus) (* 62 x8_minus) (* (- 19) x5_plus) (* 19 x5_minus) (* (- 24) x3_plus) (* 24 x3_minus) (* (- 49) x2_plus) (* 49 x2_minus) ) (- 35) ) ) (check-sat) (exit)