[SMT-COMP] Update use of `--decision` option (#8922)

The name of the mode changed from justification-stoponly to just
stoponly.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 6980d31f2a17d75b2d84469810737fccb0b29da6..2426693bfd16adba27d5bddc7caf575b22a5dd43 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -136,7 +136,7 @@ LIA|LRA)
   ;;
 QF_AUFBV)
   trywith 600
-  finishwith --decision=justification-stoponly
+  finishwith --decision=stoponly
   ;;
 QF_ABV)
   trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
@@ -157,7 +157,7 @@ QF_AUFNIA)
   ;;
 QF_ALIA)
   trywith 140 --decision=justification --arrays-weak-equiv
-  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  finishwith --decision=stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_S|QF_SLIA)
   trywith 300 --strings-exp --strings-fmf --no-jh-rlv-order

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 75e3bfc8270cd384dbc32608279cccc1ae90b115..0ecb6b62cab835263fb3b30d7af947c4a3ad4a9e 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -39,7 +39,7 @@ NIA|NRA)
   finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  finishwith --decision=justification-stoponly
+  finishwith --decision=stoponly
   ;;
 QF_ABV)
   finishwith --arrays-weak-equiv
@@ -60,7 +60,7 @@ QF_AUFNIA)
   finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_ALIA)
-  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  finishwith --decision=stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_S|QF_SLIA)
   finishwith --strings-exp