diff --git a/what4/CHANGES.md b/what4/CHANGES.md
index 892ab402..f0a3f068 100644
--- a/what4/CHANGES.md
+++ b/what4/CHANGES.md
@@ -1,3 +1,8 @@
+# next
+
+* `What4.Utils.ResolveBounds.BV.resolveSymBV` no longer requires the width of
+  the bitvector as an explicit `NatRepr` argument. The argument can be removed.
+
 # 1.5.1 (October 2023)
 
 * Require building with `versions >= 6.0.2`.
diff --git a/what4/src/What4/Utils/ResolveBounds/BV.hs b/what4/src/What4/Utils/ResolveBounds/BV.hs
index b0e4daf7..963515c1 100644
--- a/what4/src/What4/Utils/ResolveBounds/BV.hs
+++ b/what4/src/What4/Utils/ResolveBounds/BV.hs
@@ -97,15 +97,13 @@ resolveSymBV ::
   -> SearchStrategy
      -- ^ The strategy to use when searching for lower and upper bounds. For
      --   many use cases, 'ExponentialSearch' is a reasonable default.
-  -> PN.NatRepr w
-     -- ^ The bitvector width
   -> WPO.SolverProcess scope solver
      -- ^ The online solver process to use to search for lower and upper
      --   bounds.
   -> WI.SymBV sym w
      -- ^ The bitvector to resolve.
   -> IO (ResolvedSymBV w)
-resolveSymBV sym searchStrat w proc symBV =
+resolveSymBV sym searchStrat proc symBV =
   -- First check, if the SymBV can be trivially resolved as concrete. If so,
   -- this can avoid the need to call out to the solver at all.
   case WI.asBV symBV of
@@ -154,6 +152,8 @@ resolveSymBV sym searchStrat w proc symBV =
                 (BV.asUnsigned lowerBound) (BV.asUnsigned upperBound)
         else pure $ BVConcrete modelForBV
   where
+    w = WI.bvWidth symBV
+
     conn :: WPS.WriterConn scope solver
     conn = WPO.solverConn proc