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 (file)
index d809e7e..0000000
--- 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 (file)
index 0000000..c1f65e5
--- /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)