diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-30 21:13:37 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-30 21:13:37 -0700 |
| commit | 8cfc5cf2a170f32153f9cc3823dc8339d37086c3 (patch) | |
| tree | 65f582ded662c6bfec0e770b5a752dfc2b8942a1 /contrib | |
| parent | 6edc06b3fb6367e8366cab13340228e2bebfca1e (diff) | |
Remove invalid options from run scripts (#6645)
This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation | 2 | ||||
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation index 338215a52..b5df43b72 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -20,7 +20,7 @@ QF_LIA) finishwith --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 --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_BV) - finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction ;; *) # just run the default diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index ab6e2a6fc..d87e83257 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -51,7 +51,7 @@ QF_UFBV) finishwith ;; QF_BV) - finishwith --bv-div-zero-const --no-bv-abstraction + finishwith --no-bv-abstraction ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification @@ -66,7 +66,7 @@ QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) - finishwith --strings-exp --rewrite-divk + finishwith --strings-exp ;; QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp |