diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-13 17:41:42 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-13 17:41:42 -0400 |
| commit | f6dd7379078de253a6ec5cc3302f78010dbfccc3 (patch) | |
| tree | 860aaf1b06dc734ff1d0a04caabd44d53494af71 /contrib/run-script-smtcomp2014 | |
| parent | 57e44de6cc08f36743fe46a2ae4ff8810029e5c4 (diff) | |
Doubly-ensure incremental is off in main track. Also import bv-portfolio strategy.
Diffstat (limited to 'contrib/run-script-smtcomp2014')
| -rwxr-xr-x | contrib/run-script-smtcomp2014 | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/contrib/run-script-smtcomp2014 b/contrib/run-script-smtcomp2014 index a6c53c1cd..cd81a3f52 100755 --- a/contrib/run-script-smtcomp2014 +++ b/contrib/run-script-smtcomp2014 @@ -11,7 +11,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_] # function returns normally. function trywith { limit=$1; shift; - result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-checking --no-interactive "$@" $bench)" + result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench)" case "$result" in sat|unsat) echo "$result"; exit 0;; esac @@ -20,7 +20,7 @@ function trywith { # use: finishwith [params..] # to run cvc4 and let it output whatever it will to stdout. function finishwith { - $cvc4 -L smt2 --no-checking --no-interactive "$@" $bench + $cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench } case "$logic" in @@ -70,10 +70,16 @@ QF_AUFBV) finishwith --decision=justification-stoponly ;; QF_BV) - trywith 10 --bv-eq-slicer=auto --decision=justification - trywith 60 --decision=justification - trywith 600 --decision=internal --bitblast-eager - finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 + exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive \ + --threads 2 \ + --thread0 '--unconstrained-simp --bv-eq-slicer=auto' \ + --thread1 '--bitblast=eager --unconstrained-simp' \ + --no-wait-to-join \ + "$bench" + #trywith 10 --bv-eq-slicer=auto --decision=justification + #trywith 60 --decision=justification + #trywith 600 --decision=internal --bitblast-eager + #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1 ;; QF_AUFLIA|QF_AX) finishwith --no-arrays-eager-index --arrays-eager-lemmas |