diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-28 10:28:38 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-28 10:28:38 -0700 |
| commit | 77ace5eaacaf1e98a4732e163848f2f8fbfbf219 (patch) | |
| tree | cd8e321606aa042f9a6aeb7c2ed1cb872c5094a5 /contrib | |
| parent | 8254206aa9898e2c66a32f65dc19069b11cc6460 (diff) | |
Updated incremental run script
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2016-application | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/contrib/run-script-smtcomp2016-application b/contrib/run-script-smtcomp2016-application index 9dd79ba00..88bbb5f53 100644 --- a/contrib/run-script-smtcomp2016-application +++ b/contrib/run-script-smtcomp2016-application @@ -20,33 +20,32 @@ 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?) - $cvc4 --force-logic="$logic" -L smt2 --print-success --no-checking --no-interactive --incremental "$@" <&0- + $cvc4 --force-logic="$logic" -L smt2 --print-success --no-checking --no-interactive "$@" <&0- } case "$logic" in -QF_LRA) - 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 +ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA) + runcvc4 --incremental ;; -QF_LIA) - # same as QF_LRA but add --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 +ANIA|QF_ANIA|QF_NIA|QF_UFNIA) + runcvc4 --tear-down-incremental=1 ;; -ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) - runcvc4 --simplification=none --decision=internal --full-saturate-quant +LIA) + runcvc4 --incremental --cbqi ;; -LIA|LRA|NIA|NRA) - runcvc4 --enable-cbqi --full-saturate-quant +QF_AUFLIA) + runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental ;; QF_BV) - runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 + runcvc4 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 ;; -QF_AUFLIA|QF_AX) - runcvc4 --no-arrays-eager-index --arrays-eager-lemmas +QF_LIA) + runcvc4 --tear-down-incremental=1 --unconstrained-simp ;; *) # just run the default - runcvc4 + runcvc4 --incremental ;; esac |