diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8e919ac2969..cd1d66e017f 100644
--- 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
index b96cde8be98..f5bc1d556d4 100644
--- 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"