diff options
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 |