diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,8 @@
+# 1.7.3 -- 2026-01-26
+
+* Fix a bug in which `what4`'s Bitwuzla adapter would generate invalid code
+  involving SMT arrays.
+
 # 1.7.2 (November 2025)
 
 * Fix a regression in `what4-1.7.1` in which `sbvToInteger` could compute
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
@@ -1166,7 +1166,8 @@
   ComplexToArrayTypeMap  -> return ()
   PrimArrayTypeMap args ret ->
     do traverseFC_ (declareTypes conn) args
-       declareStructDatatype conn args
+       when (supportedFeatures conn `hasProblemFeature` useStructs) $
+         declareStructDatatype conn args
        declareTypes conn ret
   FnArrayTypeMap args ret ->
     do traverseFC_ (declareTypes conn) args
diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs
--- a/test/ExprBuilderSMTLib2.hs
+++ b/test/ExprBuilderSMTLib2.hs
@@ -52,6 +52,7 @@
 import           What4.Protocol.SMTLib2
 import           What4.SatResult
 import           What4.Solver.Adapter
+import qualified What4.Solver.Bitwuzla as Bitwuzla
 import qualified What4.Solver.CVC4 as CVC4
 import qualified What4.Solver.CVC5 as CVC5
 import qualified What4.Solver.Z3 as Z3
@@ -141,6 +142,18 @@
     (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
     (\(_,s) -> action sym s)
 
+withBitwuzla
+  :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer Bitwuzla.Bitwuzla) -> IO a)
+  -> IO a
+withBitwuzla action = withSym FloatRealRepr $ \sym -> do
+  extendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym)
+  bracket
+    (do h <- if debugOutputFiles then Just <$> openFile "bitwuzla.out" WriteMode else return Nothing
+        s <- startSolverProcess (defaultFeatures Bitwuzla.Bitwuzla) h sym
+        return (h,s))
+    (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
+    (\(_,s) -> action sym s)
+
 withModel
   :: Session t Z3.Z3
   -> BoolExpr t
@@ -1260,7 +1273,7 @@
 main :: IO ()
 main = do
   testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"
-  let solverNames = SolverName <$> [ "cvc4", "cvc5", "yices", "z3" ]
+  let solverNames = SolverName <$> [ "bitwuzla", "cvc4", "cvc5", "yices", "z3" ]
   solvers <- reportSolverVersions testLevel id
              =<< (zip solverNames <$> mapM getSolverVersion solverNames)
   let z3Tests =
@@ -1380,6 +1393,9 @@
         , testCase "Yices #315 test case" $ withYices issue315Test
         , testCase "Yices #329 test case" $ withYices issue329Test
         ]
+  let bitwuzlaTests =
+        [ testCase "Bitwuzla multidim array" $ withBitwuzla multidimArrayTest
+        ]
   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id
                             else fmap (ignoreTestBecause (nm <> " not present"))
   defaultMain $ testGroup "Tests" $
@@ -1399,6 +1415,7 @@
     , testUnsafeSetAbstractValue1
     , testUnsafeSetAbstractValue2
     ]
+    <> (skipIfNotPresent "bitwuzla" bitwuzlaTests)
     <> (skipIfNotPresent "cvc4" cvc4Tests)
     <> (skipIfNotPresent "cvc5" cvc5Tests)
     <> (skipIfNotPresent "yices" yicesTests)
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.2
+Version:       1.7.3
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com
 Copyright:     (c) Galois, Inc 2014-2023