Update options for SMT-COMP (#6704)

This commit removes obsolete options for BV and strings logics, and
updates QF_NIA to spend more time on our best configuration.

Co-authored-by: Gereon Kremer nafur42@gmail.com
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com

4 files changed, 21 insertions, 24 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index ea3b2dde1..db72b3a6b 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -56,23 +56,23 @@ 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 --pb-rewrites --ite-simp --simp-ite-compress
   ;;
 QF_NIA)
-  trywith 480 --nl-ext-tplanes --decision=internal
-  trywith 60 --nl-ext-tplanes --decision=justification
+  trywith 420 --nl-ext-tplanes --decision=justification
+  trywith 60 --nl-ext-tplanes --decision=internal
+  trywith 60 --nl-ext-tplanes --decision=justification-old
   trywith 60 --no-nl-ext-tplanes --decision=internal
   trywith 60 --no-arith-brab --nl-ext-tplanes --decision=internal
   # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail
-  trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
-  trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=2 --bitblast=eager
+  trywith 300 --solve-int-as-bv=4 --bitblast=eager
+  trywith 300 --solve-int-as-bv=8 --bitblast=eager
+  trywith 300 --solve-int-as-bv=16 --bitblast=eager
+  trywith 600 --solve-int-as-bv=32 --bitblast=eager
   finishwith --nl-ext-tplanes --decision=internal
   ;;
 QF_NRA)
-  trywith 300 --nl-ext-tplanes --decision=internal
-  trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
-  trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int
-  finishwith --nl-ext-tplanes --decision=justification
+  trywith 600 --decision=justification
+  trywith 300 --decision=internal --no-nl-cad --nl-ext=full --nl-ext-tplanes
+  finishwith --decision=internal --nl-ext=none
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA)
@@ -140,13 +140,10 @@ QF_ABV)
   finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
   ;;
 QF_UFBV)
-  # Benchmarks with uninterpreted sorts cannot be solved with eager
-  # bit-blasting currently
-  trywith 1200 --bitblast=eager --bv-sat-solver=cadical
-  finishwith
+  finishwith --bitblast=eager
   ;;
 QF_BV)
-  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  finishwith --bitblast=eager --bv-assert-input
   ;;
 QF_AUFLIA)
   finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
@@ -162,8 +159,8 @@ QF_ALIA)
   finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_S|QF_SLIA)
-  trywith 300 --strings-exp --rewrite-divk --strings-fmf --no-jh-rlv-order
-  finishwith --strings-exp --rewrite-divk --no-jh-rlv-order
+  trywith 300 --strings-exp --strings-fmf --no-jh-rlv-order
+  finishwith --strings-exp --no-jh-rlv-order
   ;;
 QF_ABVFP|QF_ABVFPLRA)
   finishwith --fp-exp
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index e0b51bc46..c6901ff5b 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -38,7 +38,7 @@ QF_AUFLIA)
   runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_BV)
-  runcvc5 --incremental --bitblast=eager --bv-sat-solver=cadical
+  runcvc5 --incremental --bitblast=eager --bv-assert-input
   ;;
 QF_UFBV)
   runcvc5 --incremental
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 b5df43b72..fe8d4ae44 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 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  finishwith --bitblast=eager --bv-assert-input
   ;;
 *)
   # 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 d87e83257..e9753781d 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -17,7 +17,7 @@ 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 --ite-simp --simp-ite-compress
+  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
   ;;
 QF_NIA)
   finishwith --nl-ext --nl-ext-tplanes
@@ -42,16 +42,16 @@ NIA|NRA)
   finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  finishwith --decision=justification-stoponly --ite-simp
+  finishwith --decision=justification-stoponly
   ;;
 QF_ABV)
-  finishwith --ite-simp --simp-with-care --arrays-weak-equiv
+  finishwith --arrays-weak-equiv
   ;;
 QF_UFBV)
   finishwith
   ;;
 QF_BV)
-  finishwith --no-bv-abstraction
+  finishwith
   ;;
 QF_AUFLIA)
   finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification