diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-05-25 11:02:32 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-25 11:02:32 -0700 |
| commit | d7e4d90e547427f511dfabb66bf3686cb987324b (patch) | |
| tree | ba9747b9eed5a2a2a82bb92f9c2b6c1065e94604 | |
| parent | 6c16f1ea3dbe82ddaeeb1180836cce9aedea2f29 (diff) | |
Add QF_BV configuration for SMTCOMP'18. (#1981)
| -rw-r--r-- | contrib/run-script-smtcomp2018 | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018 index b920152b2..5264bc26c 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -116,16 +116,7 @@ QF_UFBV) finishwith --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_BV) - exec ./pcvc4 -L smt2.6 --no-incremental --no-checking --no-interactive --thread-stack=1024 \ - --threads 2 \ - --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-abstraction' \ - --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \ - --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 + finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-abstraction --bv-eq-slicer=auto ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification |