summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/competitions/smt-comp/run-script-smtcomp-current-model-validation2
-rwxr-xr-xcontrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores4
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback