Support to test the "dumper" mechanism in regressions (feeding dump output back in...

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 4b365d9f2624048018e8ed5d970eb4d790687af1..9245bb0af66b4f14358151094660381baf8b35da 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = . arith precedence uf uflra uflia bv arrays datatypes lemmas push-pop
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index d6b2b143a1f1e59d3144d761053bc6d5294f846b..7136662e660fc0c86f351588fe548d40dd63c86c 100644 (file)
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = . integers
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index d55e12fbc1b806da8f5041e97f69c9873e1cfd16..eb3a9dba5d737c8b98ff43413913fca22634e9ba 100644 (file)
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -1,9 +1,9 @@
 SUBDIRS = .
 
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4
 else
-TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index 137b5bb6df5ce172f760eb371e553ce21b94f568..b112d11290a3962ced2716240cf4606dd2baa67b 100644 (file)
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -1,7 +1,7 @@
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4
 endif
 
 # These are run for all build profiles.

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 1cdfec8fc9688a26e307e9307408bac44db7f0b3..7b9ff2efcd0c0ac53aec9e5ef01c9bc98e9eb144 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = . core
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 6a36f518830fbe130f8c8454b4bd7af6781ab1bd..f58b01bc230f927ded9a51292af1ceb6dd7bcb8f 100644 (file)
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -1,8 +1,8 @@
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 58189753568c9aa081c944e7ddcc8642a6955558..a98901435db3c4f5d39f6affc87a91d0c3ce893b 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -1,9 +1,9 @@
 SUBDIRS = .
 
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am
index 94104ed49ba6d77c2d13e59a4aaf0506f2333810..7f8bbd39762d3e58f20a5b15457d8fb512743c41 100644 (file)
--- a/test/regress/regress0/lemmas/Makefile.am
+++ b/test/regress/regress0/lemmas/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = .
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 719b196cad4f87710936dcc3968ba59c97502dae..9957ade25f3693b87e3b5ac66c2724c4a5e477e2 100644 (file)
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,8 +1,8 @@
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.

diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 85d188515f04a83ab4caf676038bcbac3c893264..2a6c17eaef8d0f491e5be759bcb118a18edf2ab5 100644 (file)
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -1,9 +1,9 @@
 SUBDIRS = . 
 
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/cvc4
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/cvc4
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index f43a4d1834944b70675b594341c637a7705533e0..413b8c60a453ba68c56670d4d9cf413a8ff10432 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = .
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index e7dae10808c86a10ee0dcfb48d0310487121c36e..3eef0f3ce2e7fe2286785f279ac4a48ca63248bc 100644 (file)
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,8 +1,8 @@
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.

diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am
index e27f2d1e3e1afa710459af71af4ea3a819964620..11f1f8da33d6643ef4be5f2f6a674acc15636ce8 100644 (file)
--- a/test/regress/regress0/uflia/Makefile.am
+++ b/test/regress/regress0/uflia/Makefile.am
@@ -1,8 +1,8 @@
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index f32e980adc208aedb92f17170d597f0cf1cfc267..4817582c0bc7f147bc82f2e61b83216c224177ea 100644 (file)
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -1,8 +1,8 @@
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index 2135cf55b0e4ed67c587e60ce79acb6ba9af8eea..a8483484ec6a5b556eaeecec00f8398c8013fd50 100644 (file)
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = . arith
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am
index 3eb33d31106b7bc9a31648499d7bbd4fc33f9ee8..d831059dbea5a35d8be9529bef4f5e71e2d00118 100644 (file)
--- a/test/regress/regress1/arith/Makefile.am
+++ b/test/regress/regress1/arith/Makefile.am
@@ -1,8 +1,8 @@
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 # These are run for all build profiles.

diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 53866b5b79ddc66c1e80b782255715bed767af0e..23243d9d2c23f9aacd9dd28e9199343734ec6689 100644 (file)
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = .
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 201e332d1c84aed6bfe20a97d01b2407786b2d44..b1345b8d90549e731fa5ed5f85b3151f04a8d645 100644 (file)
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -2,9 +2,9 @@ SUBDIRS = .
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
-TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
 else
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/$(BINARY)
+TESTS_ENVIRONMENT = @srcdir@/../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
 MAKEFLAGS = -k

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 75d81b938464dd92ce36016862835f474aa84ea3..81570e817694d6677dc7bd67b585c2a1b1805d2e 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -5,7 +5,7 @@
 #
 # usage:
 #
-#     run_regression cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
+#     run_regression cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
 #
 # Runs benchmark and checks for correct exit status and output.
 #
@@ -13,14 +13,18 @@
 prog=`basename "$0"`
 
 if [ $# -lt 2 -o $# -gt 3 ]; then
-  echo "usage: $prog cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
+  echo "usage: $prog cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
   exit 1
 fi
 
 proof=no
+dump=no
 if [ $1 = --proof ]; then
   proof=yes
   shift
+elif [ $1 = --dump ]; then
+  dump=yes
+  shift
 fi
 
 cvc4=$1
@@ -179,11 +183,19 @@ if [ -z "$cvc4dirfull" ]; then
 fi
 cvc4base=`basename "$cvc4"`
 cvc4full="$cvc4dirfull/$cvc4base"
-echo running $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"`;
-  echo $? >"$exitstatusfile"
-) > "$outfile" 2> "$errfile"
+if [ $dump = no ]; then
+  echo running $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"`;
+    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"`]
+  ( 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 -;
+    echo $? >"$exitstatusfile"
+  ) > "$outfile" 2> "$errfile"
+fi
 
 diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"`
 diffexit=$?