some fixes for win32, including ability to "make check" win32 builds via wine

diff --git a/configure.ac b/configure.ac
index 6af7cf97c496e21fda653c18791023f1aac6859e..bf5938e7016e61541466daa0308237fd32ca78b5 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -1125,11 +1125,16 @@ CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 # visibility flag not supported for Windows builds
+# also increase default stack size for Windows binaries
 case $host_os in
   (*mingw*) FLAG_VISIBILITY_HIDDEN=
+            cvc4_LDFLAGS=-Wl,--stack,134217728
+            pcvc4_LDFLAGS=-Wl,--stack,134217728
 esac
 
 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
+AC_SUBST(cvc4_LDFLAGS)
+AC_SUBST(pcvc4_LDFLAGS)
 
 # mk_include
 #

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 952951655132eeceeb5efcb9c49a2c07ef294bd0..64a43eb027e9589645d078e6ccf471fe61a97283 100644 (file)
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -41,9 +41,9 @@ pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread
 pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
 
 if STATIC_BINARY
-pcvc4_LINK = $(CXXLINK) -all-static
+pcvc4_LINK = $(CXXLINK) -all-static $(pcvc4_LDFLAGS)
 else
-pcvc4_LINK = $(CXXLINK)
+pcvc4_LINK = $(CXXLINK) $(pcvc4_LDFLAGS)
 endif
 endif
 
@@ -87,8 +87,8 @@ clean-local:
        rm -f $(BUILT_SOURCES)
 
 if STATIC_BINARY
-cvc4_LINK = $(CXXLINK) -all-static
+cvc4_LINK = $(CXXLINK) -all-static $(cvc4_LDFLAGS)
 else
-cvc4_LINK = $(CXXLINK)
+cvc4_LINK = $(CXXLINK) $(cvc4_LDFLAGS)
 endif
 

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 9aca3cb5abcc2f895bea93ac79f0ba4f56cebc9f..32aa33bed6cc0611f8ded94c29328a64de0fcf1a 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -42,8 +42,6 @@ namespace CVC4 {
 class ExprManager;
 class SmtEngine;
 
-inline std::ostream& operator<<(std::ostream& os, const timespec& t);
-
 /**
  * The base class for all statistics.
  *
@@ -620,6 +618,8 @@ public:
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
 
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
 /** Compute the sum of two timespecs. */
 inline timespec& operator+=(timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d5b35594fe7807823ca1b97ebb9483cd97df34bd..3fd793b40077d91859f17e0aeea4cf33e010082b 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -3,7 +3,7 @@ DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatype
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 38e7e6f4ee492e6c7aded8c221e183144b283654..4df0543f5c4b1687c3fe23140ab4581a0c842786 100644 (file)
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = . integers
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index de7ccebce9cf02e05fc42e59e4108cb07bb14a0e..88e9c5fbdf83bc5dcb5e6a5ab5504168f450b524 100644 (file)
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 3e6fe860d0b7d6a1fcda06aff17be3b720a6bd23..e8642bc4fdad8051e96add80fc3022356205fd1b 100644 (file)
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index 23dabffcb15e30261d26e76c2611ea6eb83b4c59..937123bf7435de37e8934b4f6f86da686f14f385 100644 (file)
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index 8ed9096c49e5080cab7ac52920e963f2acbee726..d58798b9826276a18be8bf97e2cccd334b115061 100644 (file)
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 2b8b082077fd19c0bf81bf2e55a08551706f08f6..5d3fe371ebfa97e28cf4f6802110f12f9cb66c9b 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = . core
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 7960c459ac0b1ba5446bed812877b062291fafc7..53cdadc4f3460911601e0b5e6e1a913571120aa3 100644 (file)
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 58bd6711df72b967920047a32c8476970e33d859..e733bae521ae43354af20e66813c54893831b912 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 1eeea55c110e0f582bb28dd597db26acc22d05f6..4bba7b0493316ce51d6436ae4157b925f1c9c1c8 100644 (file)
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am
index 040c089594c33cd36ec4de931bdaeb390e52597d..126b206abcd718af88d0fe99d0b3674504ee7410 100644 (file)
--- a/test/regress/regress0/lemmas/Makefile.am
+++ b/test/regress/regress0/lemmas/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 0e2e3937f75f1e6fb2a3dc86d5fe64750fd952f7..4b8b4a05d748d2da9547c0e968451927e4530efa 100644 (file)
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 8351132a04fe48d8d4065bba6ca91ae92b2a0609..96b5d292874a58387d3f2817bf867843775a2aaf 100644 (file)
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 5123eca449c393a5edf043b155ab936127a1a0f5..409bef064ae7ebfe0349aebfd0c676061c558eea 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = boolean arith .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/push-pop/arith/Makefile.am b/test/regress/regress0/push-pop/arith/Makefile.am
index 37a6e6c425d29eda7dedc7f9f32d51ea50f78fe0..7171e6e210444a758ff2dc8c502d5b72acb4e1e2 100644 (file)
--- a/test/regress/regress0/push-pop/arith/Makefile.am
+++ b/test/regress/regress0/push-pop/arith/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/push-pop/boolean/Makefile.am b/test/regress/regress0/push-pop/boolean/Makefile.am
index 63b791aedc62a8a329665be849353875e5a837f6..5b12f59fa8045accab0a8710b5827c72a770cd8c 100644 (file)
--- a/test/regress/regress0/push-pop/boolean/Makefile.am
+++ b/test/regress/regress0/push-pop/boolean/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 914f596aed144f61b956674a24d2a50c029987c8..112da2a6e3e0bcc481e5a87aee69970e75775294 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index f0d45c28370ef10f1db495d6324578bd2679e7a0..1750887336fd7a90142121a484a0c12cafe30a4b 100644 (file)
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -1,10 +1,9 @@
-BINARY = cvc4
-
 CVC4_REGRESSION_ARGS ?= --efficient-e-matching
 export CVC4_REGRESSION_ARGS
 
+BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 9af43f9a44e66d1622854a7ee3ca2a6c76eeae9a..66ce8e3e6b65df8401602778dcd15a3dc3861bc7 100644 (file)
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am
index 27487b962033539eab2952d62e54d6dd0a0bc438..f5ded6b88cce419373a81146d1c52bbf7242b6ca 100644 (file)
--- a/test/regress/regress0/uflia/Makefile.am
+++ b/test/regress/regress0/uflia/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 60b3109f18e82c1069497d62fa4c97889acc8d33..3491909e394597feacfda2246a94bed89cf360ef 100644 (file)
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index 7e5bcba8c6ceb1ae2638c31c1f3de805c699db14..9a6ca29baf3152e6423db390e92429f8145f61bd 100644 (file)
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index 3c88b0b0c1d48448d0bffe52c29b9ddca9a6b76c..bcbb0a61801dff4c911f139a20f27615033da5ae 100644 (file)
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = . arith
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am
index 729dc56707704c726e889556d94609a5d68e4d40..bfbafdd3a06ebe77a44ddfa471b0a5601968b953 100644 (file)
--- a/test/regress/regress1/arith/Makefile.am
+++ b/test/regress/regress1/arith/Makefile.am
@@ -1,6 +1,6 @@
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 95d6a35083aebc098ca53d1e3de3ddbf2085c57c..e0524b694365f8db604bd372af34aa7bbecb15ad 100644 (file)
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 8bdbcec92017d097d76075d54378bd58c2cd544d..ed3e66b20df9abcd7fcd1e0c429b5f1e5dd2fadb 100644 (file)
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -2,7 +2,7 @@ SUBDIRS = .
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 68c1e0677741735b5f3e58dc8e5968b0a7a41cbe..475cce4310b2a02f476b34eaf13eb69c2d53e042 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -12,21 +12,32 @@
 
 prog=`basename "$0"`
 
-if [ $# -lt 2 -o $# -gt 3 ]; then
-  echo "usage: $prog [ --proof | --dump ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ]" >&2
+if [ $# -lt 2 ]; then
+  echo "usage: $prog [ --proof | --dump ] [ wrapper ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ]" >&2
   exit 1
 fi
 
 proof=no
 dump=no
-if [ $1 = --proof ]; then
+if [ x"$1" = x--proof ]; then
   proof=yes
   shift
-elif [ $1 = --dump ]; then
+elif [ x"$1" = x--dump ]; then
   dump=yes
   shift
 fi
 
+if [ $# -lt 2 ]; then
+  echo "usage: $prog [ --proof | --dump ] [ wrapper ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ]" >&2
+  exit 1
+fi
+
+wrapper=
+while [ $# -gt 2 ]; do
+  wrapper="$wrapper$1 "
+  shift
+done
+
 cvc4=$1
 benchmark_orig=$2
 benchmark="$benchmark_orig"
@@ -209,15 +220,15 @@ fi
 cvc4base=`basename "$cvc4"`
 cvc4full="$cvc4dirfull/$cvc4base"
 if [ $dump = no ]; then
-  echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
+  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
   ( cd `dirname "$benchmark"`;
-    "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`;
+    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile"
 else
-  echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` \| $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 - [from working dir `dirname "$benchmark"`]
+  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` \| $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 - [from working dir `dirname "$benchmark"`]
   ( cd `dirname "$benchmark"`;
-    "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` | $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 -;
+    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` | $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --lang=smt2 -;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile"
 fi
@@ -249,9 +260,9 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then
   gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX
   cp "$benchmark" "$pfbenchmark";
   echo "$proof_command" >>"$pfbenchmark";
-  echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
+  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
   ( cd `dirname "$pfbenchmark"`;
-    "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`;
+    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile"
 
@@ -276,7 +287,7 @@ fi
 
 if $check_models; then
   # at least one sat/invalid response: run an extra model-checking pass
-  if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS --check-models" "$0" "$cvc4" "$benchmark_orig"; then
+  if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS --check-models" "$0" $wrapper "$cvc4" "$benchmark_orig"; then
     exitcode=1
   fi
 fi