From 8cfc5cf2a170f32153f9cc3823dc8339d37086c3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 30 May 2021 21:13:37 -0700 Subject: [PATCH] Remove invalid options from run scripts (#6645) This commit removes some of the options in the run scripts that are not supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of those options are effectively enabled by default in cvc5. --- NEWS | 9 +++++---- .../smt-comp/run-script-smtcomp-current-model-validation | 2 +- .../smt-comp/run-script-smtcomp-current-unsat-cores | 4 ++-- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 54575dcc2..0b78073e9 100644 --- a/NEWS +++ b/NEWS @@ -4,7 +4,6 @@ Changes since 1.8 ================= New Features: - * New unsat-core production modes based on the new proof infrastructure (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT @@ -33,9 +32,10 @@ Changes: builds will be BSD licensed. * The semantics for division and remainder operators in the CVC language now correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero - modulus results in a constant value, instead of an uninterpreted one). - Similarly, when no language is set, the API semantics now correspond to the - SMT-LIB 2.6 semantics. + modulus results in a constant value, instead of an uninterpreted one). As a + result the option `--bv-div-zero-const` has been removed. Similarly, when no + language is set, the API semantics now correspond to the SMT-LIB 2.6 + semantics. * The `competition` build type includes the dependencies used for SMT-COMP by default. Note that this makes this build type produce GPL-licensed binaries. * Bit-vector operator bvxnor was previously mistakenly marked as @@ -47,6 +47,7 @@ Changes: and does *not* begin with the keyword `model`. The output is the same as before, only with this word removed from the beginning. * Building with Python 2 is now deprecated. +* Removed the option `--rewrite-divk` (now effectively enabled by default). Changes since 1.7 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 338215a52..b5df43b72 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 --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction ;; *) # 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 ab6e2a6fc..d87e83257 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -51,7 +51,7 @@ QF_UFBV) finishwith ;; QF_BV) - finishwith --bv-div-zero-const --no-bv-abstraction + finishwith --no-bv-abstraction ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification @@ -66,7 +66,7 @@ QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) - finishwith --strings-exp --rewrite-divk + finishwith --strings-exp ;; QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp -- 2.30.2