From a211c34d77c432007c3e1ed3c82baaea315a7632 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 2 Jun 2019 19:30:10 -0700 Subject: [PATCH] [SMT-COMP 2019] Update run script for unsat cores (#3034) `--unconstrained-simp` is not compatible with unsat cores, so this commit removes it for QF_LRA. `--bitblast=eager` is not compatible with unsat cores for QF_UFBV because the dependencies are not tracked correctly in the Ackermannization preprocessing pass, so the commit changes the script to use the lazy BV solver instead. Strings need some additional options to use the correct theory symbols. --- contrib/run-script-smtcomp2019-unsat-cores | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores index 1454e7a8a..78ec6ba22 100755 --- a/contrib/run-script-smtcomp2019-unsat-cores +++ b/contrib/run-script-smtcomp2019-unsat-cores @@ -14,7 +14,7 @@ function finishwith { case "$logic" in QF_LRA) - finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp + 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 --unconstrained-simp --use-soi @@ -48,7 +48,7 @@ QF_ABV) finishwith --ite-simp --simp-with-care --arrays-weak-equiv ;; QF_UFBV) - finishwith --bitblast=eager --bv-sat-solver=cryptominisat + finishwith ;; QF_BV) finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction @@ -65,6 +65,9 @@ QF_AUFNIA) QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; +QF_S|QF_SLIA) + finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 + ;; QF_ABVFP) finishwith ;; -- 2.30.2