make dist && make distcheck functional, other fixes

21 files changed, 212 insertions, 75 deletions

diff --git a/Makefile.am b/Makefile.am
index 4048b1b41..35744e381 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -80,3 +80,21 @@ lcov lcov-all lcov18:
 
 endif
 
+# abs_srcdir is required here to get this Makefile instead of the
+# Makefile in the builddir (since $(srcdir) is stripped off of
+# EXTRA_DIST files)
+EXTRA_DIST = \
+	Makefile.builds.in \
+	Makefile.subdir \
+	config/build-type \
+	config/mkbuilddir \
+	contrib/addsourcedir \
+	contrib/code-checker \
+	contrib/configure-in-place \
+	contrib/cvc-devel.el \
+	contrib/cvc-mode.el \
+	contrib/dimacs_to_smt.pl \
+	contrib/editing-with-emacs \
+	contrib/switch-config
+dist-hook:
+	cp -p "$(srcdir)/Makefile" "$(distdir)/Makefile"
diff --git a/configure.ac b/configure.ac
index 49e35f71e..4cdeb4955 100644
--- a/configure.ac
+++ b/configure.ac
@@ -244,6 +244,9 @@ AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
 
 # construct the build string
 AC_MSG_CHECKING([for appropriate build string])
+if test -z "$ac_confdir"; then
+  ac_confdir="$srcdir"
+fi
 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
 if test "$custom_build_profile" = yes; then
   if test "$with_build" = default; then
diff --git a/src/Makefile.am b/src/Makefile.am
index 97c66ac89..e436971fa 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -42,6 +42,12 @@ libcvc4_noinst_la_LIBADD = \
 	@builddir@/smt/libsmt.la \
 	@builddir@/theory/libtheory.la
 
+EXTRA_DIST = \
+	include/cvc4parser_private.h \
+	include/cvc4parser_public.h \
+	include/cvc4_private.h \
+	include/cvc4_public.h
+
 # empty.cpp hack; see above
 empty.cpp:; touch empty.cpp
 
@@ -55,3 +61,9 @@ install-data-local: $(publicheaders)
 		echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
 		$(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
 	done
+
+uninstall-local:
+	@for f in $(publicheaders); do \
+		rm -f "$(DESTDIR)/$(includedir)/cvc4/$$f"
+	done
+	rmdir "$(DESTDIR)/$(includedir)/cvc4"
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index db863440c..5f2453898 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -10,47 +10,63 @@ libexpr_la_SOURCES = \
 	node.cpp \
 	type_node.h \
 	type_node.cpp \
+	type_constant.h \
 	node_builder.h \
 	convenience_node_builders.h \
-	@srcdir@/expr.h \
 	type.h \
 	type.cpp \
 	node_value.h \
 	node_manager.h \
-	@srcdir@/expr_manager.h \
 	attribute.h \
+	attribute_internals.h \
 	attribute.cpp \
-	@srcdir@/kind.h \
-	@srcdir@/metakind.h \
 	node_manager.cpp \
-	@srcdir@/expr_manager.cpp \
 	node_value.cpp \
-	@srcdir@/expr.cpp \
 	command.h \
 	command.cpp \
 	declaration_scope.h \
 	declaration_scope.cpp \
 	expr_manager_scope.h 
+nodist_libexpr_la_SOURCES = \
+	kind.h \
+	metakind.h \
+	expr.h \
+	expr.cpp \
+	expr_manager.h \
+	expr_manager.cpp
 
 EXTRA_DIST = \
-	@srcdir@/kind.h \
-	@srcdir@/metakind.h \
-	@srcdir@/expr_manager.h \
-	@srcdir@/expr.h \
-	@srcdir@/expr_manager.cpp \
-	@srcdir@/expr.cpp \
-	@srcdir@/type.h \
-	@srcdir@/type.cpp \
 	kind_template.h \
 	metakind_template.h \
 	expr_manager_template.h \
 	expr_manager_template.cpp \
 	expr_template.h \
-	expr_template.cpp
+	expr_template.cpp \
+	mkkind \
+	mkmetakind \
+	mkexpr
+
+BUILT_SOURCES = \
+	kind.h \
+	metakind.h \
+	expr.h \
+	expr.cpp \
+	expr_manager.h \
+	expr_manager.cpp \
+	$(top_builddir)/src/theory/.subdirs
+
+CLEANFILES = \
+	kind.h \
+	metakind.h \
+	expr.h \
+	expr.cpp \
+	expr_manager.h \
+	expr_manager.cpp \
+	$(top_builddir)/src/theory/.subdirs
 
 include @top_srcdir@/src/theory/Makefile.subdirs
 
-@srcdir@/kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkkind
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkkind \
@@ -58,7 +74,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-@srcdir@/metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkmetakind
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkmetakind \
@@ -66,7 +82,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -74,7 +90,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -82,7 +98,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -90,34 +106,10 @@ include @top_srcdir@/src/theory/Makefile.subdirs
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
 		$< \
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
-
-BUILT_SOURCES = \
-	@srcdir@/kind.h \
-	@srcdir@/metakind.h \
-	@srcdir@/expr.h \
-	@srcdir@/expr.cpp \
-	@srcdir@/expr_manager.h \
-	@srcdir@/expr_manager.cpp
-
-dist-hook: \
-	@srcdir@/kind.h \
-	@srcdir@/metakind.h \
-	@srcdir@/expr.h \
-	@srcdir@/expr.cpp \
-	@srcdir@/expr_manager.h \
-	@srcdir@/expr_manager.cpp
-
-MAINTAINERCLEANFILES = \
-	@srcdir@/kind.h \
-	@srcdir@/metakind.h \
-	@srcdir@/expr.h \
-	@srcdir@/expr.cpp \
-	@srcdir@/expr_manager.h \
-	@srcdir@/expr_manager.cpp
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 2318699e7..83462c355 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -19,7 +19,7 @@
 #ifndef DECLARATION_SCOPE_H_
 #define DECLARATION_SCOPE_H_
 
-#include "expr.h"
+#include "expr/expr.h"
 #include "util/hash.h"
 
 #include <ext/hash_map>
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index cfe983727..ea67ef356 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -28,8 +28,10 @@ libparsercvc_la_SOURCES = \
     cvc_input.cpp \
     $(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
 	-$(AM_V_at)rmdir @srcdir@/generated
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index f5ea3aae3..19665b0f7 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -30,8 +30,10 @@ libparsersmt_la_SOURCES = \
 	smt_input.cpp \
 	$(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
 	-$(AM_V_at)rmdir @srcdir@/generated
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index aabae5352..99ff0daba 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -25,13 +25,15 @@ ANTLR_STUFF = \
 libparsersmt2_la_SOURCES = \
 	Smt2.g \
 	smt2.h \
-    smt2.cpp \
+	smt2.cpp \
 	smt2_input.h \
 	smt2_input.cpp \
 	$(ANTLR_STUFF)
 
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
 	-$(AM_V_at)rmdir @srcdir@/generated
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 06504e73c..dbd32c062 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -11,7 +11,6 @@ libprop_la_SOURCES = \
 	sat.h \
         sat.cpp \
 	cnf_stream.h \
-	cnf_stream.cpp \
-	cnf_conversion.h
+	cnf_stream.cpp
 
 SUBDIRS = minisat
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index a2a206d40..ce15b86d4 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -6,12 +6,15 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libtheory.la
 
 libtheory_la_SOURCES = \
-	@srcdir@/theoryof_table.h \
+	output_channel.h \
+	interrupted.h \
 	theory_engine.h \
 	theory_engine.cpp \
 	theory_test_utils.h \
 	theory.h \
 	theory.cpp
+nodist_libtheory_la_SOURCES = \
+	theoryof_table.h
 
 libtheory_la_LIBADD = \
 	@builddir@/builtin/libbuiltin.la \
@@ -22,12 +25,19 @@ libtheory_la_LIBADD = \
 	@builddir@/bv/libbv.la
 
 EXTRA_DIST = \
-	@srcdir@/theoryof_table.h \
-	theoryof_table_template.h
+	theoryof_table_template.h \
+	mktheoryof \
+	Makefile.subdirs
+
+BUILT_SOURCES = \
+	theoryof_table.h
+
+CLEANFILES = \
+	theoryof_table.h
 
 include @top_srcdir@/src/theory/Makefile.subdirs
 
-@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mktheoryof
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mktheoryof \
@@ -35,8 +45,4 @@ include @top_srcdir@/src/theory/Makefile.subdirs
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-BUILT_SOURCES = @srcdir@/theoryof_table.h
-dist-hook: @srcdir@/theoryof_table.h
-MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
-
 SUBDIRS = builtin booleans uf arith arrays bv
diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs
index 0dfba2449..eafb350ae 100644
--- a/src/theory/Makefile.subdirs
+++ b/src/theory/Makefile.subdirs
@@ -4,3 +4,4 @@ $(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/theory/Makefile.am
 		echo "  GEN   " $@; \
 		$(am__mv) $(top_builddir)/src/theory/.subdirs.tmp $(top_builddir)/src/theory/.subdirs; \
 	fi
+
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 4d299e8af..e500f5cf8 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -18,7 +18,6 @@ libarith_la_SOURCES = \
 	partial_model.cpp \
 	ordered_bounds_list.h \
 	basic.h \
-	normal.h \
 	slack.h \
 	tableau.h \
 	arith_propagator.h \
@@ -26,4 +25,6 @@ libarith_la_SOURCES = \
 	theory_arith.h \
 	theory_arith.cpp
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds \
+	normal_form_notes.txt
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b6ca5bcc6..a690f7432 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -16,6 +16,7 @@ libutil_la_SOURCES = \
 	decision_engine.h \
 	exception.h \
 	hash.h \
+	bool.h \
 	model.h \
 	options.h \
 	output.cpp \
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index de06dd4d2..a3808b751 100644
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,5 +1,5 @@
 SUBDIRS = regress0
-DIST_SUBDIRS = regress1 regress2 regress3
+DIST_SUBDIRS = regress0 regress1 regress2 regress3
 
 export VERBOSE = 1
 
@@ -13,3 +13,7 @@ regress0 regress1 regress2 regress3:
 # synonyms for "check"
 .PHONY: regress test
 regress test: check
+
+EXTRA_DIST = \
+	run_regression \
+	README
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 4744cc0fe..47ff97d61 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -63,12 +63,18 @@ TESTS =	\
 	wiki.21.cvc \
 	fuzz_3.smt
 
+EXTRA_DIST = $(TESTS)
+
 if CVC4_BUILD_PROFILE_COMPETITION
 else
 TESTS += \
 	error.cvc
 endif
 
+# and make sure to distribute it
+EXTRA_DIST += \
+	error.cvc
+
 # synonyms for "check"
 .PHONY: regress regress0 test
 regress regress0 test: check
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 362ec70b6..4cf18f17d 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,6 +1,10 @@
 TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+
+# 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 = \
-    iff-implies.cvc \
+	iff-implies.cvc \
 	implies-iff.cvc \
 	implies-or.cvc \
 	or-implies.cvc \
@@ -16,6 +20,17 @@ TESTS = \
 	implies-assoc.cvc \
 	xor-assoc.cvc
 
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 802189f2b..bf516107e 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,4 +1,8 @@
 TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+
+# 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 =	\
 	euf_simp01.smt \
 	euf_simp02.smt \
@@ -15,10 +19,22 @@ TESTS =	\
 	dead_dnd002.smt \
 	iso_brn001.smt \
 	SEQ032_size2.smt \
-    simple.01.cvc \
-    simple.02.cvc \
-    simple.03.cvc \
-    simple.04.cvc
+	simple.01.cvc \
+	simple.02.cvc \
+	simple.03.cvc \
+	simple.04.cvc
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index f133a272d..981ab8012 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -12,11 +12,17 @@ TESTS =	friedman_n4_i5.smt \
 	fuzz_1.smt \
 	fuzz_2.smt
 
+EXTRA_DIST = $(TESTS)
+
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
 #	error.cvc
 #endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
 
 # synonyms for "check"
 .PHONY: regress regress1 test
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 9dd4934ac..51d145859 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -22,11 +22,17 @@ TESTS =	bmc-galileo-8.smt \
 	hole9.cvc \
 	qwh.35.405.shuffled-as.sat03-1651.smt
 
+EXTRA_DIST = $(TESTS)
+
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
 #	error.cvc
 #endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
 
 # synonyms for "check"
 .PHONY: regress regress2 test
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 5d34df14d..8d3ebb137 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -10,11 +10,17 @@ TESTS =	C880mul.miter.shuffled-as.sat03-348.smt \
 	hole10.cvc \
 	instance_1151.smt
 
+EXTRA_DIST = $(TESTS)
+
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
 #	error.cvc
 #endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
 
 # synonyms for "check"
 .PHONY: regress regress3 test
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index e427e3506..c96fbccb6 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -40,7 +40,8 @@ export VERBOSE = 1
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
 TEST_DEPS_DIST = \
-	memory.h
+	memory.h \
+	Makefile.tests
 
 if HAVE_CXXTESTGEN
 
@@ -68,6 +69,8 @@ AM_LIBADD_PUBLIC = \
 
 EXTRA_DIST = \
 	no_cxxtest \
+	$(UNIT_TESTS:%=%.cpp) \
+	$(UNIT_TESTS:%=%.h) \
 	$(TEST_DEPS_DIST)
 
 MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
@@ -133,15 +136,19 @@ else
 TESTS = no_cxxtest
 
 EXTRA_DIST = \
-	$(UNIT_TESTS:%=%.cpp) \
-	$(TEST_DEPS_DIST)
+	no_cxxtest \
+	$(UNIT_TESTS:%=%.h) \
+	$(TEST_DEPS_DIST) \
+	no-cxxtest-available
 
 endif
 
+$(UNIT_TESTS:%=%.cpp): $(UNIT_TESTS:%=$(abs_builddir)/%.cpp)
+
 # trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
 if CVC4_FALSE
 noinst_LTLIBRARIES = libdummy.la
-libdummy_la_SOURCES = expr/node_black.cpp
+nodist_libdummy_la_SOURCES = expr/node_black.cpp
 libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 endif
 
@@ -152,3 +159,35 @@ regress test: check
 # in unit test dir, regressN are also synonyms for check
 .PHONY: regress0 regress1 regress2 regress3
 regress0 regress1 regress2 regress3: check
+
+if HAVE_CXXTESTGEN
+# all is fine with the world
+else
+# all is not !
+no-cxxtest-available:
+	@if test "$(I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS)" = 1; then \
+		echo; \
+		echo "WARNING:"; \
+		echo "WARNING: No CxxTest to build unit tests, but, then, you know that;"; \
+		echo "WARNING: I hope you know what you're doing."; \
+		echo "WARNING:"; \
+		echo; \
+		( echo "CxxTest was not available at the time this distribution was built,"; \
+		  echo "so the tests could not be built.  You'll need CxxTest to test this"; \
+		  echo "distribution." ) >no-cxxtest-available; \
+	else \
+		echo; \
+		echo "ERROR:"; \
+        	echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
+        	echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
+		echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \
+		echo "ERROR: distribution built correctly."; \
+		echo "ERROR: If you really want to do this, append the following to your make command."; \
+		echo "ERROR:"; \
+        	echo "ERROR:     I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
+		echo "ERROR:"; \
+		echo; \
+		exit 1; \
+	fi >&2
+endif
+