(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 x3_plus () Int)
(declare-fun x3_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)
(declare-fun x2_plus () Int)
(declare-fun x2_minus () Int)
(declare-fun x4_plus () Int)
(declare-fun x4_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 (>= x3_plus 0))
(assert (>= x3_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 (>= x2_plus 0))
(assert (>= x2_minus 0))
(assert (>= x4_plus 0))
(assert (>= x4_minus 0))
(assert (<= (+ (* 9 x9_plus) (* (- 9) x9_minus) (* 7 x8_plus) (* (- 7) x8_minus) (* (- 1) x7_plus) x7_minus (* (- 1) x5_plus) x5_minus (* (- 6) x3_plus) (* 6 x3_minus) (* (- 2) x1_plus) (* 2 x1_minus) (* (- 2) x0_plus) (* 2 x0_minus) ) (- 3) ) )
(assert (<= (+ (* 6 x9_plus) (* (- 6) x9_minus) (* 9 x8_plus) (* (- 9) x8_minus) (* 2 x7_plus) (* (- 2) x7_minus) (* 9 x6_plus) (* (- 9) x6_minus) (* (- 2) x5_plus) (* 2 x5_minus) (* 4 x2_plus) (* (- 4) x2_minus) (* (- 8) x0_plus) (* 8 x0_minus) ) (- 8) ) )
(assert (<= (+ (* 8 x9_plus) (* (- 8) x9_minus) (* (- 3) x6_plus) (* 3 x6_minus) (* (- 3) x4_plus) (* 3 x4_minus) (* (- 5) x3_plus) (* 5 x3_minus) (* (- 4) x2_plus) (* 4 x2_minus) (* (- 1) x1_plus) x1_minus (* 2 x0_plus) (* (- 2) x0_minus) ) 9 ) )
(assert (<= (+ (* 2 x8_plus) (* (- 2) x8_minus) (* 2 x7_plus) (* (- 2) x7_minus) (* (- 2) x6_plus) (* 2 x6_minus) (* (- 7) x5_plus) (* 7 x5_minus) (* 2 x3_plus) (* (- 2) x3_minus) (* 6 x1_plus) (* (- 6) x1_minus) (* (- 7) x0_plus) (* 7 x0_minus) ) (- 5) ) )
(assert (<= (+ (* 5 x9_plus) (* (- 5) x9_minus) x8_plus (* (- 1) x8_minus) (* (- 12) x6_plus) (* 12 x6_minus) (* (- 6) x2_plus) (* 6 x2_minus) x1_plus (* (- 1) x1_minus) (* 8 x0_plus) (* (- 8) x0_minus) ) 8 ) )
(assert (<= (+ (* 18 x9_plus) (* (- 18) x9_minus) (* 7 x8_plus) (* (- 7) x8_minus) (* 7 x6_plus) (* (- 7) x6_minus) (* (- 6) x2_plus) (* 6 x2_minus) (* (- 13) x1_plus) (* 13 x1_minus) ) 0 ) )
(assert (<= (+ (* 4 x5_plus) (* (- 4) x5_minus) (* 13 x4_plus) (* (- 13) x4_minus) (* (- 4) x3_plus) (* 4 x3_minus) (* 5 x1_plus) (* (- 5) x1_minus) ) (- 6) ) )
(assert (<= (+ x9_plus (* (- 1) x9_minus) (* 8 x4_plus) (* (- 8) x4_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* (- 6) x0_plus) (* 6 x0_minus) ) 5 ) )
(assert (>= (+ (* 8 x8_plus) (* (- 8) x8_minus) (* 3 x7_plus) (* (- 3) x7_minus) (* (- 2) x6_plus) (* 2 x6_minus) (* (- 6) x4_plus) (* 6 x4_minus) (* (- 6) x3_plus) (* 6 x3_minus) (* 2 x1_plus) (* (- 2) x1_minus) (* (- 8) x0_plus) (* 8 x0_minus) ) 6 ) )
(assert (>= (+ (* 9 x9_plus) (* (- 9) x9_minus) (* (- 5) x6_plus) (* 5 x6_minus) (* 3 x5_plus) (* (- 3) x5_minus) (* 7 x4_plus) (* (- 7) x4_minus) (* (- 2) x2_plus) (* 2 x2_minus) (* 8 x1_plus) (* (- 8) x1_minus) (* 10 x0_plus) (* (- 10) x0_minus) ) (- 8) ) )
(assert (>= (+ (* 5 x9_plus) (* (- 5) x9_minus) (* 9 x8_plus) (* (- 9) x8_minus) (* (- 1) x7_plus) x7_minus (* (- 8) x6_plus) (* 8 x6_minus) (* 4 x5_plus) (* (- 4) x5_minus) (* (- 4) x3_plus) (* 4 x3_minus) (* (- 2) x1_plus) (* 2 x1_minus) ) (- 1) ) )
(assert (>= (+ (* 4 x9_plus) (* (- 4) x9_minus) (* 2 x7_plus) (* (- 2) x7_minus) (* (- 1) x5_plus) x5_minus (* (- 4) x4_plus) (* 4 x4_minus) (* (- 3) x3_plus) (* 3 x3_minus) (* (- 7) x0_plus) (* 7 x0_minus) ) 8 ) )
(assert (>= (+ (* 7 x9_plus) (* (- 7) x9_minus) (* 3 x8_plus) (* (- 3) x8_minus) (* 4 x6_plus) (* (- 4) x6_minus) (* 12 x3_plus) (* (- 12) x3_minus) (* 8 x2_plus) (* (- 8) x2_minus) (* 9 x1_plus) (* (- 9) x1_minus) ) 4 ) )
(assert (>= (+ (* 11 x9_plus) (* (- 11) x9_minus) (* 2 x7_plus) (* (- 2) x7_minus) (* (- 3) x5_plus) (* 3 x5_minus) (* 3 x3_plus) (* (- 3) x3_minus) (* 6 x1_plus) (* (- 6) x1_minus) (* (- 1) x0_plus) x0_minus ) 7 ) )
(assert (>= (+ (* 3 x8_plus) (* (- 3) x8_minus) (* 6 x5_plus) (* (- 6) x5_minus) (* (- 8) x4_plus) (* 8 x4_minus) (* 3 x3_plus) (* (- 3) x3_minus) (* 2 x2_plus) (* (- 2) x2_minus) (* 5 x1_plus) (* (- 5) x1_minus) ) 3 ) )
(assert (>= (+ (* 7 x8_plus) (* (- 7) x8_minus) (* 9 x7_plus) (* (- 9) x7_minus) (* 5 x6_plus) (* (- 5) x6_minus) (* (- 3) x5_plus) (* 3 x5_minus) (* 10 x1_plus) (* (- 10) x1_minus) ) 4 ) )
(assert (>= (+ x6_plus (* (- 1) x6_minus) (* 5 x4_plus) (* (- 5) x4_minus) (* (- 2) x2_plus) (* 2 x2_minus) (* (- 9) x1_plus) (* 9 x1_minus) (* 7 x0_plus) (* (- 7) x0_minus) ) 5 ) )
(assert (>= (+ (* 8 x9_plus) (* (- 8) x9_minus) (* (- 4) x7_plus) (* 4 x7_minus) (* (- 12) x5_plus) (* 12 x5_minus) (* 2 x4_plus) (* (- 2) x4_minus) (* (- 7) x0_plus) (* 7 x0_minus) ) 0 ) )
(assert (>= (+ (* 8 x9_plus) (* (- 8) x9_minus) (* 3 x7_plus) (* (- 3) x7_minus) (* (- 5) x4_plus) (* 5 x4_minus) (* 5 x2_plus) (* (- 5) x2_minus) ) 5 ) )
(assert (>= (+ (* 3 x7_plus) (* (- 3) x7_minus) (* (- 13) x6_plus) (* 13 x6_minus) (* 2 x4_plus) (* (- 2) x4_minus) (* (- 3) x1_plus) (* 3 x1_minus) ) 2 ) )
(check-sat)
(exit)