diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,8 @@
+# 1.7.2 (November 2025)
+
+* Fix a regression in `what4-1.7.1` in which `sbvToInteger` could compute
+  incorrect results for symbolic bitvectors.
+
 # 1.7.1 (November 2025)
 
 * Add `asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)`
diff --git a/src/What4/Protocol/SMTWriter.hs b/src/What4/Protocol/SMTWriter.hs
--- a/src/What4/Protocol/SMTWriter.hs
+++ b/src/What4/Protocol/SMTWriter.hs
@@ -1599,8 +1599,15 @@
           -> v
           -> v
 bvIntTerm w x = sumExpr digits
- where -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in
-       -- bvIntTerm's type signature.
+ where -- Note that the `1 <= w` constraint in `bvIntTerm`'s type signature is
+       -- a slightly stronger assumption that what is needed here. This
+       -- definition would also work if `w == 0`, since `[1..natValue w]` would
+       -- evaluate to an empty list, producing no digits (as expected). Since
+       -- nearly every bitvector-related operation in what4 assumes `1 <= w`,
+       -- we include the constraint here as well for consistency.
+       --
+       -- Contrast this with the definition of `digits` in `sbvIntTerm`, where
+       -- the `1 <= w` assumption in crucial.
        digits :: [v]
        digits = (\i -> digit (i-1)) <$> [1..natValue w]
 
@@ -1611,8 +1618,10 @@
 
 -- @sbvIntTerm w x@ builds an integer term that has the same value as the
 -- signed integer value of the bitvector @x@. This is done by explicitly
--- decomposing the positional notation of the bitvector into a sum of powers of
--- 2, plus an offset to ensure that the number is signed appropriately.
+-- decomposing the positional notation of the bitvector's @w-1@ least
+-- significant bits into a sum of powers of 2, plus an offset (based on whether
+-- the most significant bit is set or not) to ensure that the number is signed
+-- appropriately.
 sbvIntTerm :: forall v w
             . (SupportTermOps v, 1 <= w)
            => NatRepr w
@@ -1626,8 +1635,18 @@
                           (fromInteger (negate (2^(widthVal w - 1))))
                           0
 
+       -- Note that unlike the corresponding `digits` value in `bvIntTerm`,
+       -- this `digits` value only takes the @w-1@ least significant bits of
+       -- `x` into consideration, as the most significant bit is used to
+       -- compute `signedOffset` instead.
+       --
+       -- NB: If `w == 1`, then `[1..(natValue w - 1)]` will evaluate to an
+       -- empty list, producing no digits (as expected).
+       --
+       -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in
+       -- sbvIntTerm's type signature.
        digits :: [v]
-       digits = (\i -> digit (i-1)) <$> [1..natValue w]
+       digits = (\i -> digit (i-1)) <$> [1..(natValue w - 1)]
 
        digit :: SupportTermOps v => Natural -> v
        digit d = ite (bvTestBit w d x)
diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs
--- a/test/ExprBuilderSMTLib2.hs
+++ b/test/ExprBuilderSMTLib2.hs
@@ -1114,6 +1114,40 @@
 
       _ -> fail "expected satisfible model"
 
+-- | A regression test for #329.
+issue329Test ::
+  OnlineSolver solver =>
+  SimpleExprBuilder t fs ->
+  SolverProcess t solver ->
+  IO ()
+issue329Test sym solver = do
+    -- This test shows that the following proposition (written in Cryptol) is
+    -- falsifiable when `x == 2`:
+    --
+    --   \(x : [2]) -> x == 2 ==> ((toSignedInteger x - 1) == -1)
+    let w = knownNat @2
+    x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)
+    bvTwo <- bvLit sym w (BV.mkBV w 2)
+    xEqBvTwo <- bvEq sym x bvTwo
+    notXEqBvTwo <- notPred sym xEqBvTwo
+    xsi <- sbvToInteger sym x
+    intOne <- intLit sym 1
+    intNegOne <- intLit sym (-1)
+    xsiDec <- intSub sym xsi intOne
+    xsiDecEqIntNegOne <- intEq sym xsiDec intNegOne
+    p <- orPred sym notXEqBvTwo xsiDecEqIntNegOne
+
+    -- Check if `p` is not valid for all `x` by checking if its negation
+    -- (`notP`) is satisfiable. If `notP` is satisfiable, then we have found a
+    -- counterexample to `p`.
+    notP <- notPred sym p
+    checkSatisfiableWithModel solver "test" notP $ \case
+      Sat fn ->
+        do xEval <- groundEval fn x
+           (xEval == BV.mkBV w 2) @? "result other than 2"
+
+      _ -> fail "expected satisfible model"
+
 -- | These tests simply ensure that no exceptions are raised.
 testSolverInfo :: TestTree
 testSolverInfo = testGroup "solver info queries" $
@@ -1277,6 +1311,7 @@
 
         , testCase "Z3 #182 test case" $ withOnlineZ3 issue182Test
         , testCase "Z3 #315 test case" $ withOnlineZ3 issue315Test
+        , testCase "Z3 #329 test case" $ withOnlineZ3 issue329Test
 
         , arrayCopyTest
         , arraySetTest
@@ -1328,6 +1363,7 @@
 
         , cvcTestCase "#182 test case" $ withCVC issue182Test
         , cvcTestCase "#315 test case" $ withCVC issue315Test
+        , cvcTestCase "#329 test case" $ withCVC issue329Test
         ]
   let cvc4Tests = cvcTests CVC4
   let cvc5Tests = cvcTests CVC5
@@ -1342,6 +1378,7 @@
         , testCase "Yices rounding" $ withYices roundingTest
         , testCase "Yices #182 test case" $ withYices issue182Test
         , testCase "Yices #315 test case" $ withYices issue315Test
+        , testCase "Yices #329 test case" $ withYices issue329Test
         ]
   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id
                             else fmap (ignoreTestBecause (nm <> " not present"))
diff --git a/what4.cabal b/what4.cabal
--- a/what4.cabal
+++ b/what4.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.4
 Name:          what4
-Version:       1.7.1.0
+Version:       1.7.2
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com
 Copyright:     (c) Galois, Inc 2014-2023