minor

yoni206 · Aug 19, 2024 · 206445c · 206445c
1 parent 5a67009
commit 206445c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
@@ -282,6 +282,8 @@ TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
       res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
     }
   }
+  // When int-blasting, it is better to handle most overflow operators
+  // natively, rather than to eliminate them eagerly.
   if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF)
   {
     res = d_rewriter.eliminateOverflows(res);

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
@@ -16,7 +16,6 @@
 #include "theory/bv/theory_bv_rewriter.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"