now passes "make distcheck", which does important checks for the release (e.g., ...

diff --git a/Makefile.am b/Makefile.am
index b72c710319323a00526e70d7fe66079e27432886..b3cd37e9a83ec70e60bd65fc715bf639d18203b6 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -126,3 +126,11 @@ dist-hook:
 
 distclean-local:
        test -z "$(DX_DOCDIR)" || rm -fr "$(DX_DOCDIR)"
+
+# these have .in versions
+DISTCLEANFILES = \
+       doc/cvc4.1 \
+       doc/cvc4.5 \
+       doc/libcvc4.3 \
+       doc/libcvc4compat.3 \
+       doc/libcvc4parser.3

diff --git a/src/Makefile.am b/src/Makefile.am
index 818acfa291c02c7e3e88291249e3e80d54f93e0d..e04910804156229e87bb3b32fe26c75175258445 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -146,3 +146,31 @@ uninstall-local:
        -rmdir "$(DESTDIR)$(includedir)/cvc4/bindings"
        -rmdir "$(DESTDIR)$(includedir)/cvc4"
        -rmdir "$(DESTDIR)$(libdir)/ocaml/cvc4"
+
+# clean up the .fix files
+mostlyclean-local:
+       (echo include/cvc4.h; \
+        echo include/cvc4_public.h; \
+        echo include/cvc4parser_public.h; \
+        find * -name '*.h.fix' | \
+               xargs grep -l '^# *include  *<cvc4/cvc4.*_public\.h>' | \
+               sed 's,\.fix$$,,'; \
+       (cd "$(srcdir)" && find * -name '*.h' | \
+               xargs grep -l '^# *include  *"cvc4.*_public\.h"')) | \
+       while read f; do \
+               if expr "$$f" : ".*_\(template\|private\|test_utils\)\.h$$" &>/dev/null; then \
+                       continue; \
+               fi; \
+               d="$$(echo "$$f" | sed 's,^include/,,')"; \
+               if [ -e "$$f" ]; then \
+                       path="$$f"; \
+                       fixpath="$$f.fix"; \
+               else \
+                       path="$(srcdir)/$$f"; \
+                       fixpath="$(builddir)/$$f.fix"; \
+                       $(MKDIR_P) "`dirname "$$fixpath"`"; \
+               fi; \
+               echo rm -f "$$fixpath"; \
+               rm -f "$$fixpath"; \
+       done
+

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index bcc6a28a9e86a82728e2eab7eacbb51a86133345..fcef044dcdf4fcc3d4bb399b842ce2db1f7e4a56 100644 (file)
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -36,7 +36,26 @@ TESTS =      \
 #      pp-regfile.smt \
 #
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+       aufbv-fuzz01.smt.expect \
+       pp-regfile.delta01.smt.expect \
+       uflia-error0.smt2.expect \
+       bitvec0.delta01.smt.expect \
+       pp-regfile.delta02.smt.expect \
+       uflia-xs-09-16-3-4-1-5.delta03.smt.expect \
+       bitvec0.smt.expect \
+       pp-regfile.smt.expect \
+       uflia-xs-09-16-3-4-1-5.smt.expect \
+       bitvec5.smt.expect \
+       quant-Arrays_Q1-noinfer.smt2.expect \
+       wchains010ue.delta02.smt.expect \
+       bug347.smt.expect \
+       quant-ex1.disable_miniscope.smt2.expect \
+       wchains010ue.smt.expect \
+       just_sat.expect \
+       quant-ex1.smt2.expect \
+       just_unsat.expect \
+       quant-symmetric_unsat_7.smt2.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else

diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 070f696396152b80abd0219b56f412b6102312d9..fb39acc4c55e2c6ece027c01cf104c1f89576ab8 100644 (file)
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -43,6 +43,8 @@ EXTRA_DIST = \
        $(CPLUSPLUS_TESTS:%=%.cpp) \
        $(TEST_DEPS_DIST)
 
+MOSTLYCLEANFILES = $(TESTS)
+
 if STATIC_BINARY
 system_LINK = $(CXXLINK) -all-static
 else

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index dc53bff6135fed9fd4f5be32f3c8872523baa01d..d5b6ce5bf031fe651fab088d78d45b307e2eccaa 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -105,7 +105,25 @@ EXTRA_DIST = \
        $(UNIT_TESTS:%=%.h) \
        $(TEST_DEPS_DIST)
 
-MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
+MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) $(UNIT_TESTS:%=%.lo)
+
+# the tests automake infrastructure doesn't clean up .o files :-(
+# handle both .libs and _libs variants
+mostlyclean-local:
+       @for f in $(UNIT_TESTS); do \
+               dir="$$(dirname "$$f")"; fil="$$(basename "$$f")"; \
+               for junk in     "$$dir/.libs/$$fil.o" \
+                               "$$dir/_libs/$$fil.o" \
+                               "$$dir/.libs/lt-$$fil" \
+                               "$$dir/_libs/lt-$$fil" \
+                               "$$dir/.libs/$$fil" \
+                               "$$dir/_libs/$$fil"; do \
+                       if test -e "$$junk"; then \
+                               echo "rm -f \"$$junk\""; \
+                               rm -f "$$junk"; \
+                       fi; \
+               done; \
+       done
 
 @mk_include@ @srcdir@/Makefile.tests
 

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 734e38b7b98c7abb5eab3ed6a188c78ddb9ce449..0fe0e93f0bf9e2cfae1cfc516f42048332bfdc29 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -362,7 +362,7 @@ public:
     TS_ASSERT(unnamed.hasAttribute(TestFlag5()));
 
     // test two-arg version of hasAttribute()
-    bool bb CVC4_UNUSED;
+    bool bb = false;
     Debug("boolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);