summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-06-17 09:56:39 -0400
committerlianah <lianahady@gmail.com>2014-06-19 18:24:39 -0400
commitd9804eeaa2394fd413c39ae2f63a508784280a02 (patch)
treefa7caf53d7a1cd0c86d1830f870616571538a2e7
parent0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 (diff)
Test portfolio with --no-wait-to-join.
-rw-r--r--.travis.yml2
-rw-r--r--Makefile2
2 files changed, 2 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml
index 18204d3c6..082a746c5 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -43,7 +43,7 @@ script:
make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
}
makeCheckPortfolio() {
- make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= ||
+ make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-wait-to-join --no-early-exit' RUN_REGRESSION_ARGS= ||
error "PORTFOLIO TEST FAILED";
}
makeExamples() {
diff --git a/Makefile b/Makefile
index f0541bfae..50d85d37a 100644
--- a/Makefile
+++ b/Makefile
@@ -161,7 +161,7 @@ submission-parallel:
../../configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl; \
$(MAKE) V=1; \
strip src/main/pcvc4; \
- $(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS=--fallback-sequential || true )
+ $(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-wait-to-join' || true )
# package the parallel track zipfile
mkdir -p cvc4-smtcomp-parallel-$(YEAR)/bin
cp -p builds-smtcomp/parallel/src/main/pcvc4 cvc4-smtcomp-parallel-$(YEAR)/bin/pcvc4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback