KevinMidboe/linguist
1
0
Fork 0
mirror of https://github.com/KevinMidboe/linguist.git synced 2025-12-29 21:31:01 +00:00
Code Issues Packages Projects Releases Wiki Activity

Example smt2 files

Browse Source
This commit is contained in:
Bruno Dutertre
2015-07-01 10:38:17 -07:00
parent 5f456d8b22
commit 0585c880de
4 changed files with 2267 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
samples/SMT/bignum_lia1.smt2 Normal file
View File

@@ -0,0 +1,20 @@
(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)