From 95f928be27f79efbaf8c9eea98730f1b076891a2 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 30 Jun 2022 06:45:21 -0700 Subject: [PATCH] [SMT-COMP] Update use of `--decision` option (#8922) The name of the mode changed from justification-stoponly to just stoponly. --- contrib/competitions/smt-comp/run-script-smtcomp-current | 4 ++-- .../smt-comp/run-script-smtcomp-current-unsat-cores | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 6980d31f2..2426693bf 100755 --- 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 75e3bfc82..0ecb6b62c 100755 --- 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 -- 2.30.2