Update

3 files changed, 5 insertions, 6 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 023f36c2b..db72b3a6b 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -70,10 +70,9 @@ QF_NIA)
   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)
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index bddcfcf4f..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
+  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 b35d7fb99..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
+  finishwith --bitblast=eager --bv-assert-input
   ;;
 *)
   # just run the default