[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.

diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores
index 1454e7a8a47e3d70fd62287c60b5c96aac2ff157..78ec6ba2204822e51901c574728dbe26eb388336 100755 (executable)
--- 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
   ;;