test for prvs commit (tokenize emptyset)

9978c259f30b1f4b2c70c04589a309033a6eb1f6

5 files changed, 59 insertions, 1 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 1da15dc43..236443eb9 100644
--- 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 521993db3..10148e5bc 100644
--- 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
index 000000000..be157f57a
--- /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
index 000000000..389c80e09
--- /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
index 000000000..a6e514407
--- /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)