mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
21 lines
723 B
Plaintext
21 lines
723 B
Plaintext
(set-logic QF_LIA)
|
|
(set-info :source | SMT-COMP'06 organizers |)
|
|
(set-info :smt-lib-version 2.0)
|
|
(set-info :category "check")
|
|
(set-info :status unsat)
|
|
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
|
|
(declare-fun x1 () Int)
|
|
(declare-fun x2 () Int)
|
|
(declare-fun x3 () Int)
|
|
(declare-fun x4 () Int)
|
|
(declare-fun x5 () Int)
|
|
(declare-fun x6 () Int)
|
|
(assert (and (or (>= x1 1000) (>= x1 1002))
|
|
(or (>= x2 (* 1230 x1)) (>= x2 (* 1003 x1)))
|
|
(or (>= x3 (* 1310 x2)) (>= x3 (* 1999 x2)))
|
|
(or (>= x4 (* 4000 x3)) (>= x4 (* 8000 x3)))
|
|
(or (<= x5 (* (- 4000) x4)) (<= x5 (* (- 8000) x4)))
|
|
(or (>= x6 (* (- 3) x5)) (>= x6 (* (- 2) x5))) (< x6 0)))
|
|
(check-sat)
|
|
(exit)
|