diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-22 01:23:19 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-22 01:24:13 -0400 |
| commit | ca0c712c24b745522cc8d0648b4852decb40bcb5 (patch) | |
| tree | 0ea26161424905337d0f62201223c9bb9e473877 | |
| parent | fbd3232481b8f2759daea3d683085dc038710c01 (diff) | |
Another updated submission strategy.
| -rw-r--r-- | Makefile | 2 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2014-application | 6 |
2 files changed, 4 insertions, 4 deletions
@@ -130,7 +130,7 @@ submission-application: ./autogen.sh mkdir -p builds-smtcomp/application ( cd builds-smtcomp/application; \ - ../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK; \ + ../../configure competition --disable-shared --enable-static-binary --with-cln --without-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK; \ $(MAKE) V=1; \ strip src/main/cvc4; \ $(MAKE) check ) diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index 165293e74..1a9078994 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -19,17 +19,17 @@ function runcvc4 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental --check-models "$@" + (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" } case "$logic" in QF_LRA) - runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi + runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp ;; QF_LIA) # same as QF_LRA but add --pb-rewrites - runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites + runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --pb-rewrites ;; ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) runcvc4 --simplification=none --decision=internal --full-saturate-quant |