From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 3 Jun 2019 02:30:10 +0000 (-0700)
Subject: [SMT-COMP 2019] Update run script for unsat cores (#3034)
X-Git-Tag: cvc5-1.0.0~4131
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a211c34d77c432007c3e1ed3c82baaea315a7632;p=cvc5.git

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