From ff70395fd3dcde9f68eda1c6a8bd70e6491f7458 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 19 May 2010 21:20:54 +0000
Subject: Significant revision to theory/arith.  The new draft has a lot of
 small bug fixes and organizational changes.  The theory is now enabled to
 perform checking in the TheoryEngine. This draft can now solve 2 new
 regression tests test/regress/regress0/ineq_slack.smt and
 test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside
 src/expr/attribute.h.

---
 test/regress/regress0/Makefile.am | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test/regress/regress0/Makefile.am')

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 58f9c6a4e..521536630 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -24,6 +24,8 @@ TESTS =	\
 	logops.04.cvc \
 	logops.05.cvc \
 	simple.cvc \
+	ineq_basic.smt \
+	ineq_slack.smt \
 	smallcnf.cvc \
 	test11.cvc \
 	test9.cvc \
-- 
cgit v1.2.3