test for prvs commit (tokenize emptyset)

9978c259f30b1f4b2c70c04589a309033a6eb1f6

diff --git a/test/Makefile.am b/test/Makefile.am
index 1da15dc4339569289302dbdfc2a0fb077b8cb21a..236443eb984c7f933da28b41b683dd2732e26c49 100644 (file)
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -57,6 +57,7 @@ subdirs_to_check = \
        regress/regress0/fmf \
        regress/regress0/strings \
        regress/regress0/sets \
+       regress/regress0/parser \
        regress/regress1 \
        regress/regress1/arith \
        regress/regress2 \

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 521993db3b1c5a5afb471c44ad4716776edfd16e..10148e5bc42d1adf2b2fba70ace7584919df6dfc 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser
 DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
 
 # don't override a BINARY imported from a personal.mk

diff --git a/test/regress/regress0/parser/Makefile b/test/regress/regress0/parser/Makefile
new file mode 100644 (file)
index 0000000..be157f5
--- /dev/null
+++ b/test/regress/regress0/parser/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/parser
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am
new file mode 100644 (file)
index 0000000..389c80e
--- /dev/null
+++ b/test/regress/regress0/parser/Makefile.am
@@ -0,0 +1,42 @@
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+       $(LOG_COMPILER) \
+       $(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =        \
+       declarefun-emptyset-uf.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#      error.cvc
+#endif
+
+# disabled tests, yet distribute
+#EXTRA_DIST += \
+#      setofsets-disequal.smt2
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:

diff --git a/test/regress/regress0/parser/declarefun-emptyset-uf.smt2 b/test/regress/regress0/parser/declarefun-emptyset-uf.smt2
new file mode 100644 (file)
index 0000000..a6e5144
--- /dev/null
+++ b/test/regress/regress0/parser/declarefun-emptyset-uf.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic QF_UF)
+(declare-sort T 0)
+(declare-fun union () T)
+(declare-fun emptyset () T)
+(assert (= union emptyset))
+(check-sat)