(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 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 x1_plus () Int) (declare-fun x1_minus () Int) (declare-fun x0_plus () Int) (declare-fun x0_minus () Int) (declare-fun x3_plus () Int) (declare-fun x3_minus () Int) (declare-fun x2_plus () Int) (declare-fun x2_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 (>= x6_plus 0)) (assert (>= x6_minus 0)) (assert (>= x5_plus 0)) (assert (>= x5_minus 0)) (assert (>= x4_plus 0)) (assert (>= x4_minus 0)) (assert (>= x1_plus 0)) (assert (>= x1_minus 0)) (assert (>= x0_plus 0)) (assert (>= x0_minus 0)) (assert (>= x3_plus 0)) (assert (>= x3_minus 0)) (assert (>= x2_plus 0)) (assert (>= x2_minus 0)) (assert (<= (+ (* 19 x9_plus) (* (- 19) x9_minus) (* (- 12) x8_plus) (* 12 x8_minus) (* (- 73) x7_plus) (* 73 x7_minus) (* (- 63) x6_plus) (* 63 x6_minus) (* 24 x5_plus) (* (- 24) x5_minus) (* (- 42) x4_plus) (* 42 x4_minus) (* (- 24) x1_plus) (* 24 x1_minus) (* 29 x0_plus) (* (- 29) x0_minus) ) 24 ) ) (assert (<= (+ (* 10 x9_plus) (* (- 10) x9_minus) (* (- 17) x8_plus) (* 17 x8_minus) (* 55 x7_plus) (* (- 55) x7_minus) (* 14 x5_plus) (* (- 14) x5_minus) (* (- 68) x3_plus) (* 68 x3_minus) (* (- 49) x2_plus) (* 49 x2_minus) (* 16 x1_plus) (* (- 16) x1_minus) (* (- 16) x0_plus) (* 16 x0_minus) ) 58 ) ) (assert (<= (+ (* 43 x7_plus) (* (- 43) x7_minus) (* 76 x6_plus) (* (- 76) x6_minus) (* 45 x5_plus) (* (- 45) x5_minus) (* 14 x4_plus) (* (- 14) x4_minus) (* 17 x3_plus) (* (- 17) x3_minus) (* 18 x2_plus) (* (- 18) x2_minus) (* 3 x1_plus) (* (- 3) x1_minus) (* (- 30) x0_plus) (* 30 x0_minus) ) 66 ) ) (assert (<= (+ (* 62 x9_plus) (* (- 62) x9_minus) (* (- 41) x7_plus) (* 41 x7_minus) (* 63 x6_plus) (* (- 63) x6_minus) (* 14 x5_plus) (* (- 14) x5_minus) (* (- 60) x3_plus) (* 60 x3_minus) (* (- 30) x2_plus) (* 30 x2_minus) (* 19 x1_plus) (* (- 19) x1_minus) (* 25 x0_plus) (* (- 25) x0_minus) ) 40 ) ) (assert (<= (+ (* 57 x9_plus) (* (- 57) x9_minus) (* 54 x8_plus) (* (- 54) x8_minus) (* 42 x7_plus) (* (- 42) x7_minus) (* 48 x6_plus) (* (- 48) x6_minus) (* 52 x2_plus) (* (- 52) x2_minus) (* 28 x1_plus) (* (- 28) x1_minus) (* 8 x0_plus) (* (- 8) x0_minus) ) (- 20) ) ) (assert (<= (+ x9_plus (* (- 1) x9_minus) (* (- 14) x8_plus) (* 14 x8_minus) (* 31 x7_plus) (* (- 31) x7_minus) (* (- 65) x6_plus) (* 65 x6_minus) (* 16 x2_plus) (* (- 16) x2_minus) (* (- 31) x1_plus) (* 31 x1_minus) (* 50 x0_plus) (* (- 50) x0_minus) ) (- 53) ) ) (assert (<= (+ (* 22 x9_plus) (* (- 22) x9_minus) (* (- 12) x8_plus) (* 12 x8_minus) (* 21 x6_plus) (* (- 21) x6_minus) (* 47 x4_plus) (* (- 47) x4_minus) (* (- 42) x2_plus) (* 42 x2_minus) (* (- 18) x1_plus) (* 18 x1_minus) (* 69 x0_plus) (* (- 69) x0_minus) ) (- 12) ) ) (assert (<= (+ (* 63 x9_plus) (* (- 63) x9_minus) (* 56 x8_plus) (* (- 56) x8_minus) (* (- 14) x5_plus) (* 14 x5_minus) (* (- 45) x4_plus) (* 45 x4_minus) (* 2 x3_plus) (* (- 2) x3_minus) (* 25 x2_plus) (* (- 25) x2_minus) (* (- 2) x1_plus) (* 2 x1_minus) ) 47 ) ) (assert (<= (+ (* 122 x7_plus) (* (- 122) x7_minus) (* 46 x6_plus) (* (- 46) x6_minus) (* 51 x5_plus) (* (- 51) x5_minus) (* (- 45) x4_plus) (* 45 x4_minus) (* (- 23) x3_plus) (* 23 x3_minus) (* (- 56) x0_plus) (* 56 x0_minus) ) 5 ) ) (assert (<= (+ (* 59 x9_plus) (* (- 59) x9_minus) (* (- 58) x8_plus) (* 58 x8_minus) (* 91 x7_plus) (* (- 91) x7_minus) (* 42 x4_plus) (* (- 42) x4_minus) (* (- 42) x2_plus) (* 42 x2_minus) (* 74 x0_plus) (* (- 74) x0_minus) ) 50 ) ) (assert (<= (+ (* 105 x9_plus) (* (- 105) x9_minus) x8_plus (* (- 1) x8_minus) (* (- 25) x3_plus) (* 25 x3_minus) (* (- 7) x2_plus) (* 7 x2_minus) (* 46 x1_plus) (* (- 46) x1_minus) (* 33 x0_plus) (* (- 33) x0_minus) ) 24 ) ) (assert (>= (+ (* 37 x9_plus) (* (- 37) x9_minus) (* 58 x8_plus) (* (- 58) x8_minus) (* (- 54) x7_plus) (* 54 x7_minus) (* (- 59) x6_plus) (* 59 x6_minus) (* (- 32) x4_plus) (* 32 x4_minus) (* 68 x2_plus) (* (- 68) x2_minus) (* 13 x0_plus) (* (- 13) x0_minus) ) (- 64) ) ) (assert (>= (+ (* 21 x8_plus) (* (- 21) x8_minus) (* (- 36) x5_plus) (* 36 x5_minus) (* 9 x4_plus) (* (- 9) x4_minus) (* (- 43) x3_plus) (* 43 x3_minus) (* (- 65) x1_plus) (* 65 x1_minus) (* 64 x0_plus) (* (- 64) x0_minus) ) (- 4) ) ) (assert (>= (+ (* 5 x8_plus) (* (- 5) x8_minus) (* 33 x7_plus) (* (- 33) x7_minus) (* 32 x6_plus) (* (- 32) x6_minus) (* (- 32) x3_plus) (* 32 x3_minus) (* (- 21) x2_plus) (* 21 x2_minus) (* (- 16) x0_plus) (* 16 x0_minus) ) (- 24) ) ) (assert (>= (+ (* 3 x9_plus) (* (- 3) x9_minus) (* (- 26) x8_plus) (* 26 x8_minus) (* (- 80) x7_plus) (* 80 x7_minus) (* 63 x3_plus) (* (- 63) x3_minus) (* 25 x1_plus) (* (- 25) x1_minus) (* 41 x0_plus) (* (- 41) x0_minus) ) 0 ) ) (assert (>= (+ (* 51 x6_plus) (* (- 51) x6_minus) (* 49 x5_plus) (* (- 49) x5_minus) (* 17 x3_plus) (* (- 17) x3_minus) (* (- 69) x1_plus) (* 69 x1_minus) (* 67 x0_plus) (* (- 67) x0_minus) ) (- 37) ) ) (assert (>= (+ (* 138 x7_plus) (* (- 138) x7_minus) (* 18 x6_plus) (* (- 18) x6_minus) (* 51 x4_plus) (* (- 51) x4_minus) (* 19 x1_plus) (* (- 19) x1_minus) (* (- 16) x0_plus) (* 16 x0_minus) ) 62 ) ) (assert (>= (+ (* 63 x9_plus) (* (- 63) x9_minus) (* 14 x7_plus) (* (- 14) x7_minus) (* (- 41) x5_plus) (* 41 x5_minus) (* 79 x3_plus) (* (- 79) x3_minus) (* 60 x1_plus) (* (- 60) x1_minus) ) 54 ) ) (assert (>= (+ (* 5 x9_plus) (* (- 5) x9_minus) (* (- 10) x7_plus) (* 10 x7_minus) (* (- 16) x5_plus) (* 16 x5_minus) (* (- 70) x2_plus) (* 70 x2_minus) (* (- 31) x0_plus) (* 31 x0_minus) ) (- 10) ) ) (assert (>= (+ (* 37 x6_plus) (* (- 37) x6_minus) (* (- 26) x5_plus) (* 26 x5_minus) (* 60 x4_plus) (* (- 60) x4_minus) (* 46 x3_plus) (* (- 46) x3_minus) (* 59 x2_plus) (* (- 59) x2_minus) ) 45 ) ) (check-sat) (exit)