10 files changed, 69 insertions, 11 deletions
diff --git a/Makefile.am b/Makefile.am
index e482638d3..288cfb2cc 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -89,6 +89,7 @@ EXTRA_DIST = \
 	Makefile.builds.in \
 	Makefile.subdir \
 	config/build-type \
-	config/mkbuilddir
+	config/mkbuilddir \
+	config/doxygen.cfg
 dist-hook:
 	cp -p "$(srcdir)/Makefile" "$(distdir)/Makefile"
diff --git a/src/Makefile.am b/src/Makefile.am
index a46f56598..069a446e6 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS = \
 	-I@srcdir@/include -I@srcdir@ -I@builddir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = lib expr util context theory prop smt . parser main
+SUBDIRS = lib expr util context theory prop smt printer . parser main
 
 lib_LTLIBRARIES = libcvc4.la
 noinst_LTLIBRARIES = libcvc4_noinst.la
@@ -62,15 +62,15 @@ publicheaders = \
 	include/cvc4parser_public.h
 
 install-data-local: $(publicheaders)
-	$(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4
+	$(mkinstalldirs) $(DESTDIR)$(prefix)$(includedir)/cvc4
 	@for f in $(publicheaders); do \
-		echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
-		$(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
+		echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)$(prefix)$(includedir)/cvc4"; \
+		$(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)$(prefix)$(includedir)/cvc4"; \
 	done
 
 uninstall-local:
 	@for f in $(publicheaders); do \
 		f=`echo "$$f" | sed 's,.*/,,'`; \
-		rm -f "$(DESTDIR)$(includedir)/cvc4/$$f"; \
+		rm -f "$(DESTDIR)$(prefix)$(includedir)/cvc4/$$f"; \
 	done
-	@rmdir "$(DESTDIR)$(includedir)/cvc4"
+	@rmdir "$(DESTDIR)$(prefix)$(includedir)/cvc4"
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index c82968ef6..639e9eb4c 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -3,6 +3,8 @@ AM_CPPFLAGS = \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
+SUBDIRS = builtin booleans uf arith arrays bv
+
 noinst_LTLIBRARIES = libtheory.la
 
 libtheory_la_SOURCES = \
@@ -48,5 +50,3 @@ theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory
 		$< \
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
-
-SUBDIRS = builtin booleans uf arith arrays bv
diff --git a/test/Makefile.am b/test/Makefile.am
index 2ff1c4974..e370752b6 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu='[1;34m'; \
   std='[m'; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d50633a19..9f4fdce89 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf bv lemmas
+SUBDIRS = . arith precedence uf bv lemmas push-pop
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/bv/Makefile b/test/regress/regress0/bv/Makefile
new file mode 100644
index 000000000..c9ec3204c
--- /dev/null
+++ b/test/regress/regress0/bv/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/bv
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/bv/core/Makefile b/test/regress/regress0/bv/core/Makefile
new file mode 100644
index 000000000..15e8e6220
--- /dev/null
+++ b/test/regress/regress0/bv/core/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../../..
+srcdir = test/regress/regress0/bv/core
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/lemmas/Makefile b/test/regress/regress0/lemmas/Makefile
new file mode 100644
index 000000000..96e24225b
--- /dev/null
+++ b/test/regress/regress0/lemmas/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/lemmas
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/push-pop/Makefile b/test/regress/regress0/push-pop/Makefile
new file mode 100644
index 000000000..cd5bcd3e3
--- /dev/null
+++ b/test/regress/regress0/push-pop/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../push-pop
+srcdir = test/regress/regress0/push-pop
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
new file mode 100644
index 000000000..ee365e79d
--- /dev/null
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -0,0 +1,25 @@
+SUBDIRS = . 
+
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+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 +="
+
+# Regression tests for SMT inputs
+CVC_TESTS = \
+	test.00.cvc \
+	test.01.cvc
+
+TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3: