From 31c768863403d50f7682ecbb7f72a4486de0e503 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 28 Jan 2013 09:30:12 -0500 Subject: [PATCH] some fixes for win32, including ability to "make check" win32 builds via wine --- configure.ac | 5 +++ src/main/Makefile.am | 8 ++--- src/util/statistics_registry.h | 4 +-- test/regress/regress0/Makefile.am | 2 +- test/regress/regress0/arith/Makefile.am | 2 +- .../regress0/arith/integers/Makefile.am | 2 +- test/regress/regress0/arrays/Makefile.am | 2 +- test/regress/regress0/aufbv/Makefile.am | 2 +- test/regress/regress0/auflia/Makefile.am | 2 +- test/regress/regress0/bv/Makefile.am | 2 +- test/regress/regress0/bv/core/Makefile.am | 2 +- test/regress/regress0/datatypes/Makefile.am | 2 +- test/regress/regress0/decision/Makefile.am | 2 +- test/regress/regress0/lemmas/Makefile.am | 2 +- test/regress/regress0/precedence/Makefile.am | 2 +- test/regress/regress0/preprocess/Makefile.am | 2 +- test/regress/regress0/push-pop/Makefile.am | 2 +- .../regress0/push-pop/arith/Makefile.am | 2 +- .../regress0/push-pop/boolean/Makefile.am | 2 +- test/regress/regress0/quantifiers/Makefile.am | 2 +- .../regress/regress0/rewriterules/Makefile.am | 5 ++- test/regress/regress0/uf/Makefile.am | 2 +- test/regress/regress0/uflia/Makefile.am | 2 +- test/regress/regress0/uflra/Makefile.am | 2 +- .../regress0/unconstrained/Makefile.am | 2 +- test/regress/regress1/Makefile.am | 2 +- test/regress/regress1/arith/Makefile.am | 2 +- test/regress/regress2/Makefile.am | 2 +- test/regress/regress3/Makefile.am | 2 +- test/regress/run_regression | 33 ++++++++++++------- 30 files changed, 60 insertions(+), 45 deletions(-) diff --git a/configure.ac b/configure.ac index 6af7cf97c..bf5938e70 100644 --- 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 952951655..64a43eb02 100644 --- 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 9aca3cb5a..32aa33bed 100644 --- 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 d5b35594f..3fd793b40 100644 --- 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 38e7e6f4e..4df0543f5 100644 --- 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 de7ccebce..88e9c5fbd 100644 --- 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 3e6fe860d..e8642bc4f 100644 --- 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 23dabffcb..937123bf7 100644 --- 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 8ed9096c4..d58798b98 100644 --- 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 2b8b08207..5d3fe371e 100644 --- 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 7960c459a..53cdadc4f 100644 --- 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 58bd6711d..e733bae52 100644 --- 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 1eeea55c1..4bba7b049 100644 --- 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 040c08959..126b206ab 100644 --- 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 0e2e3937f..4b8b4a05d 100644 --- 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 8351132a0..96b5d2928 100644 --- 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 5123eca44..409bef064 100644 --- 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 37a6e6c42..7171e6e21 100644 --- 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 63b791aed..5b12f59fa 100644 --- 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 914f596ae..112da2a6e 100644 --- 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 f0d45c283..175088733 100644 --- 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 9af43f9a4..66ce8e3e6 100644 --- 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 27487b962..f5ded6b88 100644 --- 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 60b3109f1..3491909e3 100644 --- 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 7e5bcba8c..9a6ca29ba 100644 --- 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 3c88b0b0c..bcbb0a618 100644 --- 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 729dc5670..bfbafdd3a 100644 --- 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 95d6a3508..e0524b694 100644 --- 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 8bdbcec92..ed3e66b20 100644 --- 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 68c1e0677..475cce431 100755 --- 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 -- 2.30.2