From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 24 May 2022 18:05:40 +0000 (-0700)
Subject: bv: Disable rule ExtractArith. (#8816)
X-Git-Tag: cvc5-1.0.1~101
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fde84aa1af32f9cc10162292886baf22293c3820;p=cvc5.git

bv: Disable rule ExtractArith. (#8816)
---

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index a4bed7c4a..cee50824d 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -76,14 +76,6 @@ name   = "Bitvector Theory"
   default    = "true"
   help       = "lift equivalence with one-bit bit-vectors to be boolean operations"
 
-[[option]]
-  name       = "bvExtractArithRewrite"
-  category   = "expert"
-  long       = "bv-extract-arith"
-  type       = "bool"
-  default    = "false"
-  help       = "enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)"
-
 [[option]]
   name       = "bvIntroducePow2"
   category   = "expert"
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index dcf24d38d..3069b12c0 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -251,13 +251,6 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
 
-  if (options::bvExtractArithRewrite()) {
-    if (RewriteRule<ExtractArith>::applies(node)) {
-      resultNode = RewriteRule<ExtractArith>::run<false>(node);
-      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-    }
-  }
-
   resultNode = LinearRewriteStrategy<
       // We could have an extract over extract
       RewriteRule<ExtractExtract>,