From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 31 May 2021 04:13:37 +0000 (-0700)
Subject: Remove invalid options from run scripts (#6645)
X-Git-Tag: cvc5-1.0.0~1672
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8cfc5cf2a170f32153f9cc3823dc8339d37086c3;p=cvc5.git

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.
---

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