bv: Disable rule ExtractArith. (#8816)

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index a4bed7c4a6751e9f92fbc3c3b9a721256bed510e..cee50824d94375f3217028d570d1fc95e81513ff 100644 (file)
--- 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 dcf24d38dda6bacaabbd5dfc4fd5ce19afc82cc9..3069b12c0bbcc347533ef0169d4944f93fa67ba2 100644 (file)
--- 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>,