From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 3 May 2010 22:08:29 +0000 (+0000)
Subject: more reasonable smt 2.0 benchmark test
X-Git-Tag: cvc5-1.0.0~9085
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69c2d3e702f8ec0bd0eec4a481a07571131aabeb;p=cvc5.git

more reasonable smt 2.0 benchmark test
---

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)