summaryrefslogtreecommitdiff
path: root/test/regress/regress0/push-pop
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2011-07-05 16:21:50 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2011-07-05 16:21:50 +0000
commit7342d1ca87397f3d5beb2c04b819243303e69a7c (patch)
tree9e166f1884275be7d4b33b13b8bcfe9418e61033 /test/regress/regress0/push-pop
parentaf25c3f8498198dd6dd114c3b4ef39af54611e1e (diff)
updated preprocessing and rewriting input equalities into inequalities for LRA
Diffstat (limited to 'test/regress/regress0/push-pop')
-rw-r--r--test/regress/regress0/push-pop/Makefile.am6
1 files changed, 2 insertions, 4 deletions
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 3a57ada3f..85c3cb9c9 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -8,13 +8,11 @@ MAKEFLAGS = -k
# put it below in "TESTS +="
# Regression tests for SMT inputs
-CVC_TESTS = \
- test.00.cvc
+CVC_TESTS =
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
-EXTRA_DIST = $(TESTS) \
- test.01.cvc
+EXTRA_DIST = $(TESTS)
# synonyms for "check" in this directory
.PHONY: regress regress0 test
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback