From 69c2d3e702f8ec0bd0eec4a481a07571131aabeb Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 3 May 2010 22:08:29 +0000
Subject: [PATCH] more reasonable smt 2.0 benchmark test

---
 test/regress/regress0/bignum_quant.smt2 | 13 -------------
 test/regress/regress0/simple.smt2       |  8 ++++++++
 2 files changed, 8 insertions(+), 13 deletions(-)
 delete mode 100644 test/regress/regress0/bignum_quant.smt2
 create mode 100644 test/regress/regress0/simple.smt2

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)
-- 
2.30.2