diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-05-03 22:08:29 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-05-03 22:08:29 +0000 |
| commit | 69c2d3e702f8ec0bd0eec4a481a07571131aabeb (patch) | |
| tree | ab0106368a6e8e9f1b08c9c26176b556c87d01db /test/regress/regress0 | |
| parent | 2c978719ce07be5f6494934363809a36de6ab24a (diff) | |
more reasonable smt 2.0 benchmark test
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/bignum_quant.smt2 | 13 | ||||
| -rw-r--r-- | test/regress/regress0/simple.smt2 | 8 |
2 files changed, 8 insertions, 13 deletions
diff --git a/test/regress/regress0/bignum_quant.smt2 b/test/regress/regress0/bignum_quant.smt2 deleted file mode 100644 index d809e7e9a..000000000 --- a/test/regress/regress0/bignum_quant.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-info :source | SMT-COMP'06 organizers |) -(set-info :smt-lib-version 2.0) -(set-info :category "check") -(set-info :status unsat) -(set-logic AUFLIA) -(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.| ) -(set-info :difficulty 0.000) -(declare-fun f (Int) Int) -(assert (= (f 0) 1)) -(assert (forall (?x Int) (=> (> ?x 0) (= (f ?x) (* (- 1000) (f (- ?x 1))))))) -(assert (< (f 20) 0)) -(check-sat) -(exit) diff --git a/test/regress/regress0/simple.smt2 b/test/regress/regress0/simple.smt2 new file mode 100644 index 000000000..c1f65e565 --- /dev/null +++ b/test/regress/regress0/simple.smt2 @@ -0,0 +1,8 @@ +(set-info :source "contrived") +(set-info :smt-lib-version 2.0) +(set-info :category "check") +(set-info :status unsat) +(set-logic QF_UF) +(set-info :notes |This benchmark simply checks that SMT-LIB v2 can be parsed.|) +(set-info :difficulty 0.000) +(exit) |