smtcomp: Change some BV configs for SQ and INC track. (#6721)

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index db72b3a6b139a0c01458cbc9166a4b6afdea3413..ecc6ce5fe4f097384c5e48b31c663ed769c1a50c 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -139,10 +139,7 @@ QF_ABV)
   trywith 500 --arrays-weak-equiv
   finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
   ;;
-QF_UFBV)
-  finishwith --bitblast=eager
-  ;;
-QF_BV)
+QF_BV|QF_UFBV)
   finishwith --bitblast=eager --bv-assert-input
   ;;
 QF_AUFLIA)

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index c6901ff5bcaebdbae01658e6a04986eea2ad0ec6..21bb2f6e0b60cd87e6c8d8dabb1cfa6d4bbcd5e7 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -41,16 +41,16 @@ QF_BV)
   runcvc5 --incremental --bitblast=eager --bv-assert-input
   ;;
 QF_UFBV)
-  runcvc5 --incremental
+  runcvc5 --incremental --bv-assert-input
   ;;
 QF_UF)
   runcvc5 --incremental
   ;;
 QF_AUFBV)
-  runcvc5 --incremental
+  runcvc5 --incremental --bv-assert-input
   ;;
 QF_ABV)
-  runcvc5 --incremental
+  runcvc5 --incremental --bv-assert-input
   ;;
 ABVFP)
   runcvc5 --incremental