diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation | 7 |
1 files changed, 6 insertions, 1 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 385a845e7..9982a9e29 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -13,6 +13,12 @@ function finishwith { case "$logic" in +QF_LRA) + finishwith --no-restrict-pivots --use-soi --new-prop + ;; +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 ;; @@ -22,4 +28,3 @@ QF_BV) ;; esac - |