(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 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 x3_plus () Int) (declare-fun x3_minus () Int) (declare-fun x0_plus () Int) (declare-fun x0_minus () Int) (declare-fun x5_plus () Int) (declare-fun x5_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 (>= x4_plus 0)) (assert (>= x4_minus 0)) (assert (>= x2_plus 0)) (assert (>= x2_minus 0)) (assert (>= x1_plus 0)) (assert (>= x1_minus 0)) (assert (>= x3_plus 0)) (assert (>= x3_minus 0)) (assert (>= x0_plus 0)) (assert (>= x0_minus 0)) (assert (>= x5_plus 0)) (assert (>= x5_minus 0)) (assert (<= (+ (* 32 x9_plus) (* (- 32) x9_minus) (* 20 x8_plus) (* (- 20) x8_minus) (* 2 x7_plus) (* (- 2) x7_minus) (* 13 x6_plus) (* (- 13) x6_minus) (* 16 x4_plus) (* (- 16) x4_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* 6 x1_plus) (* (- 6) x1_minus) ) 19 ) ) (assert (<= (+ (* 7 x8_plus) (* (- 7) x8_minus) (* 26 x7_plus) (* (- 26) x7_minus) (* 8 x6_plus) (* (- 8) x6_minus) (* (- 18) x4_plus) (* 18 x4_minus) (* (- 1) x3_plus) x3_minus (* 6 x2_plus) (* (- 6) x2_minus) (* (- 18) x0_plus) (* 18 x0_minus) ) 19 ) ) (assert (<= (+ (* 10 x9_plus) (* (- 10) x9_minus) (* (- 30) x7_plus) (* 30 x7_minus) (* (- 28) x6_plus) (* 28 x6_minus) (* 17 x5_plus) (* (- 17) x5_minus) (* (- 21) x3_plus) (* 21 x3_minus) (* (- 21) x2_plus) (* 21 x2_minus) (* (- 13) x1_plus) (* 13 x1_minus) ) (- 24) ) ) (assert (<= (+ (* 10 x9_plus) (* (- 10) x9_minus) (* 17 x8_plus) (* (- 17) x8_minus) (* 54 x6_plus) (* (- 54) x6_minus) (* (- 27) x2_plus) (* 27 x2_minus) (* (- 15) x1_plus) (* 15 x1_minus) (* (- 1) x0_plus) x0_minus ) (- 10) ) ) (assert (<= (+ (* 9 x9_plus) (* (- 9) x9_minus) (* (- 17) x7_plus) (* 17 x7_minus) (* (- 26) x6_plus) (* 26 x6_minus) (* 14 x3_plus) (* (- 14) x3_minus) (* 14 x2_plus) (* (- 14) x2_minus) (* 14 x0_plus) (* (- 14) x0_minus) ) 21 ) ) (assert (<= (+ (* 29 x9_plus) (* (- 29) x9_minus) (* 29 x7_plus) (* (- 29) x7_minus) (* 21 x6_plus) (* (- 21) x6_minus) (* (- 17) x4_plus) (* 17 x4_minus) (* 7 x1_plus) (* (- 7) x1_minus) (* 27 x0_plus) (* (- 27) x0_minus) ) 21 ) ) (assert (<= (+ x8_plus (* (- 1) x8_minus) (* 19 x7_plus) (* (- 19) x7_minus) (* (- 21) x5_plus) (* 21 x5_minus) (* (- 16) x3_plus) (* 16 x3_minus) (* 29 x1_plus) (* (- 29) x1_minus) (* (- 10) x0_plus) (* 10 x0_minus) ) 6 ) ) (assert (<= (+ (* 27 x9_plus) (* (- 27) x9_minus) (* (- 3) x6_plus) (* 3 x6_minus) (* (- 21) x5_plus) (* 21 x5_minus) (* 8 x4_plus) (* (- 8) x4_minus) (* 26 x2_plus) (* (- 26) x2_minus) (* 29 x1_plus) (* (- 29) x1_minus) ) 11 ) ) (assert (<= (+ (* 29 x9_plus) (* (- 29) x9_minus) (* 8 x5_plus) (* (- 8) x5_minus) (* (- 15) x4_plus) (* 15 x4_minus) (* 9 x2_plus) (* (- 9) x2_minus) (* 4 x1_plus) (* (- 4) x1_minus) (* (- 25) x0_plus) (* 25 x0_minus) ) 0 ) ) (assert (<= (+ (* 10 x8_plus) (* (- 10) x8_minus) (* 6 x6_plus) (* (- 6) x6_minus) (* 27 x3_plus) (* (- 27) x3_minus) (* (- 20) x2_plus) (* 20 x2_minus) (* (- 9) x1_plus) (* 9 x1_minus) (* (- 14) x0_plus) (* 14 x0_minus) ) 26 ) ) (assert (<= (+ (* 16 x9_plus) (* (- 16) x9_minus) (* (- 29) x8_plus) (* 29 x8_minus) (* (- 48) x3_plus) (* 48 x3_minus) (* 7 x2_plus) (* (- 7) x2_minus) (* 4 x1_plus) (* (- 4) x1_minus) ) 16 ) ) (assert (>= (+ (* 16 x9_plus) (* (- 16) x9_minus) (* (- 21) x8_plus) (* 21 x8_minus) (* (- 44) x7_plus) (* 44 x7_minus) (* (- 4) x6_plus) (* 4 x6_minus) (* 18 x4_plus) (* (- 18) x4_minus) (* (- 16) x3_plus) (* 16 x3_minus) (* 14 x2_plus) (* (- 14) x2_minus) (* (- 18) x0_plus) (* 18 x0_minus) ) 13 ) ) (assert (>= (+ (* 5 x9_plus) (* (- 5) x9_minus) (* 11 x8_plus) (* (- 11) x8_minus) (* (- 7) x6_plus) (* 7 x6_minus) (* 2 x5_plus) (* (- 2) x5_minus) (* 14 x4_plus) (* (- 14) x4_minus) (* (- 1) x1_plus) x1_minus (* (- 24) x0_plus) (* 24 x0_minus) ) (- 14) ) ) (assert (>= (+ (* 11 x8_plus) (* (- 11) x8_minus) (* (- 13) x7_plus) (* 13 x7_minus) (* 15 x6_plus) (* (- 15) x6_minus) (* (- 28) x5_plus) (* 28 x5_minus) x4_plus (* (- 1) x4_minus) (* (- 1) x1_plus) x1_minus (* 4 x0_plus) (* (- 4) x0_minus) ) 14 ) ) (assert (>= (+ (* 24 x8_plus) (* (- 24) x8_minus) (* 3 x7_plus) (* (- 3) x7_minus) (* (- 22) x5_plus) (* 22 x5_minus) (* (- 51) x4_plus) (* 51 x4_minus) (* 24 x3_plus) (* (- 24) x3_minus) (* (- 12) x1_plus) (* 12 x1_minus) (* 27 x0_plus) (* (- 27) x0_minus) ) 26 ) ) (assert (>= (+ (* 16 x9_plus) (* (- 16) x9_minus) (* 2 x7_plus) (* (- 2) x7_minus) (* (- 23) x6_plus) (* 23 x6_minus) (* 18 x4_plus) (* (- 18) x4_minus) (* 7 x2_plus) (* (- 7) x2_minus) (* (- 29) x1_plus) (* 29 x1_minus) (* (- 29) x0_plus) (* 29 x0_minus) ) 24 ) ) (assert (>= (+ (* 27 x8_plus) (* (- 27) x8_minus) (* (- 7) x6_plus) (* 7 x6_minus) (* 26 x4_plus) (* (- 26) x4_minus) (* (- 11) x3_plus) (* 11 x3_minus) (* (- 20) x2_plus) (* 20 x2_minus) (* (- 20) x1_plus) (* 20 x1_minus) (* (- 24) x0_plus) (* 24 x0_minus) ) 17 ) ) (assert (>= (+ (* 3 x6_plus) (* (- 3) x6_minus) (* 32 x5_plus) (* (- 32) x5_minus) (* (- 19) x4_plus) (* 19 x4_minus) (* (- 6) x2_plus) (* 6 x2_minus) (* 2 x1_plus) (* (- 2) x1_minus) (* (- 2) x0_plus) (* 2 x0_minus) ) 23 ) ) (assert (>= (+ (* 2 x9_plus) (* (- 2) x9_minus) (* (- 6) x8_plus) (* 6 x8_minus) (* 25 x5_plus) (* (- 25) x5_minus) (* (- 26) x3_plus) (* 26 x3_minus) (* (- 5) x2_plus) (* 5 x2_minus) (* (- 28) x0_plus) (* 28 x0_minus) ) (- 21) ) ) (assert (>= (+ (* 6 x9_plus) (* (- 6) x9_minus) (* 31 x8_plus) (* (- 31) x8_minus) (* 16 x4_plus) (* (- 16) x4_minus) (* (- 26) x3_plus) (* 26 x3_minus) (* (- 13) x2_plus) (* 13 x2_minus) (* (- 16) x1_plus) (* 16 x1_minus) ) 13 ) ) (check-sat) (exit)