From c29ee6ec50fb4253b449dea38ae0f122a7002672 Mon Sep 17 00:00:00 2001
From: Yoni Zohar <yoni206@gmail.com>
Date: Sun, 18 Aug 2024 20:43:22 +0300
Subject: [PATCH] Not working The rewriter is not an envobj and so i don't have
 access to the options.

---
 src/theory/bv/theory_bv.cpp                       |  1 -
 src/theory/bv/theory_bv_rewriter.cpp              | 15 +++++++++------
 test/regress/cli/regress0/bv/overflow/saddo3.smt2 |  2 +-
 test/regress/cli/regress0/bv/overflow/ssubo1.smt2 |  2 +-
 4 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index aa814be73db..5fba062ce80 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -23,7 +23,6 @@
 #include "theory/bv/bv_solver_bitblast_internal.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
 #include "theory/trust_substitutions.h"
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 01ca4b2b2bd..9f3ff4d2aef 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -15,8 +15,8 @@
 
 #include "theory/bv/theory_bv_rewriter.h"
 
-#include "options/smt_options.h"
 #include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h"
 #include "theory/bv/theory_bv_rewrite_rules_core.h"
@@ -28,7 +28,7 @@
 using namespace cvc5::internal;
 using namespace cvc5::internal::theory;
 using namespace cvc5::internal::theory::bv;
-using namespace cvc5::context;
+
 
 TheoryBVRewriter::TheoryBVRewriter(NodeManager* nm) : TheoryRewriter(nm)
 {
@@ -100,13 +100,16 @@ Node TheoryBVRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
 }
 
 TrustNode TheoryBVRewriter::expandDefinition(Node node) {
-  Node expanded = eliminateOverflows(node);
-    return TrustNode::mkTrustRewrite(node, expanded, nullptr);
+  Node expanded = node;
+  if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF) {
+    expanded = eliminateOverflows(node);
+  } 
+  return TrustNode::mkTrustRewrite(node, expanded, nullptr);
 }
 
 Node TheoryBVRewriter::eliminateOverflows(Node node) {
-  Node res = node;
-   if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF) {
+   Node res = node;
+   if (true) {
      if (RewriteRule<UaddoEliminate>::applies(node))
      {
        res = RewriteRule<UaddoEliminate>::run<false>(node);
diff --git a/test/regress/cli/regress0/bv/overflow/saddo3.smt2 b/test/regress/cli/regress0/bv/overflow/saddo3.smt2
index d6b115bc72d..99b40cb0abf 100644
--- a/test/regress/cli/regress0/bv/overflow/saddo3.smt2
+++ b/test/regress/cli/regress0/bv/overflow/saddo3.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-const v (_ BitVec 6))
-(assert (and (bvsgt v (_ bv53 6)) (not (bvsaddo v v))))
+(assert (and (bvsgt v (_ bv28 6)) (not (bvsaddo v v))))
 (check-sat)
diff --git a/test/regress/cli/regress0/bv/overflow/ssubo1.smt2 b/test/regress/cli/regress0/bv/overflow/ssubo1.smt2
index 9a8642c9f85..8014d147afb 100644
--- a/test/regress/cli/regress0/bv/overflow/ssubo1.smt2
+++ b/test/regress/cli/regress0/bv/overflow/ssubo1.smt2
@@ -4,5 +4,5 @@
 (set-logic QF_BV)
 (declare-const u (_ BitVec 6))
 (declare-const v (_ BitVec 6))
-(assert (and (bvsgt v u) (not (bvssubo u v))))
+(assert (and (bvugt v (_ bv22 6)) (bvugt (_ bv0 6) u) (not (bvssubo v u))))
 (check-sat)