diff options
| -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) |