diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,31 @@
+# 1.6 (May 2024)
+
+* Allow building with GHC 9.8.
+
+* Add more robust support for Constrained Horn Clause (CHC) solving:
+  * The `IsSymExprBuilder` class now has two additional methods,
+    `transformPredBV2LIA` and `transformSymFnLIA2BV`, which describe how to
+    transform a bitvector (BV) predicate into a linear integer arithmetic (LIA)
+    predicate and vice versa.
+  * The `runZ3Horn` and `writeZ3HornSMT2File` functions now take an additional
+    `Bool` argument. When this argument is `True`, Z3 will transform bitvector
+    CHCs into linear integer arithmetic CHCs, which can sometimes help Z3 to
+    solve CHC problems that it couldn't in a bitvector setting.
+
+* Add support for the `bitwuzla` SMT solver.
+
+* Add `bvZero` and `bvOne` functions, which are convenient shorthand for
+  constructing bitvectors with the values `0` and `1`, respectively.
+
+* Add `pushMuxOps` and `pushMuxOpsOption`. If this option is enabled, What4 will
+  push certain `ExprBuilder` operations (e.g., `zext`) down to the branches of
+  `ite` expressions. In some (but not all) circumstances, this can result in
+  operations that are easier for SMT solvers to reason about.
+
+* `annotateTerm` no longer adds annotations to bound variable expressions, which
+  already have annotations attached to them. This should result in slightly
+  better performance and better pretty-printing.
+
 # 1.5.1 (October 2023)
 
 * Require building with `versions >= 6.0.2`.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -280,6 +280,7 @@
 - Yices 2.6.1 and 2.6.2
 - CVC4 1.7 and 1.8
 - CVC5 1.0.2
+- Bitwuzla 0.3.0
 - Boolector 3.2.1 and 3.2.2
 - STP 2.3.3
     (However, note https://github.com/stp/stp/issues/363, which prevents
diff --git a/src/What4/Expr.hs b/src/What4/Expr.hs
--- a/src/What4/Expr.hs
+++ b/src/What4/Expr.hs
@@ -20,6 +20,7 @@
   , curProgramLoc
   , unaryThreshold
   , cacheStartSize
+  , pushMuxOps
   , exprBuilderSplitConfig
   , exprBuilderFreshConfig
   , EmptyExprBuilderState(..)
diff --git a/src/What4/Expr/App.hs b/src/What4/Expr/App.hs
--- a/src/What4/Expr/App.hs
+++ b/src/What4/Expr/App.hs
@@ -2114,7 +2114,7 @@
         SR.SemiRingRealRepr ->
           maybe (realLit sym 1) return =<< WSum.prodEvalM (realMul sym) return pd
         SR.SemiRingBVRepr SR.BVArithRepr w ->
-          maybe (bvLit sym w (BV.one w)) return =<< WSum.prodEvalM (bvMul sym) return pd
+          maybe (bvOne sym w) return =<< WSum.prodEvalM (bvMul sym) return pd
         SR.SemiRingBVRepr SR.BVBitsRepr w ->
           maybe (bvLit sym w (BV.maxUnsigned w)) return =<< WSum.prodEvalM (bvAndBits sym) return pd
 
@@ -2136,7 +2136,7 @@
 
     BVOrBits w bs ->
       case bvOrToList bs of
-        [] -> bvLit sym w (BV.zero w)
+        [] -> bvZero sym w
         (x:xs) -> foldM (bvOrBits sym) x xs
 
     BVTestBit i e -> testBitBV sym i e
diff --git a/src/What4/Expr/Builder.hs b/src/What4/Expr/Builder.hs
--- a/src/What4/Expr/Builder.hs
+++ b/src/What4/Expr/Builder.hs
@@ -22,6 +22,7 @@
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE EmptyCase #-}
@@ -29,6 +30,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
@@ -56,6 +58,7 @@
   , sbNonceExpr
   , curProgramLoc
   , unaryThreshold
+  , pushMuxOps
   , cacheStartSize
   , userState
   , exprCounter
@@ -74,6 +77,7 @@
     -- * configuration options
   , unaryThresholdOption
   , cacheStartSizeOption
+  , pushMuxOpsOption
   , cacheTerms
 
     -- * Expr
@@ -183,7 +187,8 @@
 import qualified Control.Exception as Ex
 import           Control.Lens hiding (asIndex, (:>), Empty)
 import           Control.Monad
-import           Control.Monad.IO.Class
+import           Control.Monad.Except
+import           Control.Monad.Reader
 import           Control.Monad.ST
 import           Control.Monad.Trans.Writer.Strict (writer, runWriter)
 import qualified Data.BitVector.Sized as BV
@@ -191,6 +196,8 @@
 import qualified Data.Bimap as Bimap
 
 import           Data.Hashable
+import qualified Data.HashTable.Class as HC
+import qualified Data.HashTable.IO as H
 import           Data.IORef
 import           Data.Kind
 import           Data.List.NonEmpty (NonEmpty(..))
@@ -331,6 +338,9 @@
   compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) =
     toOrdering $ fnCompare fn1 fn2
 
+instance Hashable (SomeExprSymFn t) where
+  hashWithSalt s (SomeExprSymFn fn) = hashWithSalt s fn
+
 instance Show (SomeExprSymFn t) where
   show (SomeExprSymFn f) = show f
 
@@ -366,6 +376,12 @@
           -- | The starting size when building a new cache
         , sbCacheStartSize :: !(CFG.OptionSetting BaseIntegerType)
 
+          -- | If enabled, push certain 'ExprBuilder' operations (e.g., @zext@)
+          -- down to the branches of @ite@ expressions. In some (but not all)
+          -- circumstances, this can result in operations that are easier for
+          -- SMT solvers to reason about.
+        , sbPushMuxOps :: !(CFG.OptionSetting BaseBoolType)
+
           -- | Counter to generate new unique identifiers for elements and functions.
         , sbExprCounter :: !(NonceGenerator IO t)
 
@@ -413,6 +429,9 @@
 cacheStartSize :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType)
 cacheStartSize = to sbCacheStartSize
 
+pushMuxOps :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType)
+pushMuxOps = to sbPushMuxOps
+
 -- | Return a new expr builder where the configuration object has
 --   been "split" using the @splitConfig@ operation.
 --   The returned sym will share any preexisting options with the
@@ -448,9 +467,11 @@
      cfg <- CFG.initialConfig 0
               [ unaryThresholdDesc
               , cacheStartSizeDesc
+              , pushMuxOpsDesc
               ]
      unarySetting       <- CFG.getOptionSetting unaryThresholdOption cfg
      cacheStartSetting  <- CFG.getOptionSetting cacheStartSizeOption cfg
+     pushMuxOpsSetting  <- CFG.getOptionSetting pushMuxOpsOption cfg
      CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg
      nonLinearOps <- newIORef 0
 
@@ -458,6 +479,7 @@
                 , sbFloatReduce = True
                 , sbUnaryThreshold = unarySetting
                 , sbCacheStartSize = cacheStartSetting
+                , sbPushMuxOps = pushMuxOpsSetting
                 , sbProgramLoc = loc_ref
                 , sbCurAllocator = storage_ref
                 , sbNonLinearOps = nonLinearOps
@@ -642,8 +664,29 @@
   where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0)
         help = Just "Maximum number of values in unary bitvector encoding."
 
+------------------------------------------------------------------------
+-- Configuration option for controlling whether to push certain ExprBuilder
+-- operations (e.g., @zext@) down to the branches of @ite@ expressions.
 
+-- | If this option enabled, push certain 'ExprBuilder' operations (e.g.,
+-- @zext@) down to the branches of @ite@ expressions. In some (but not all)
+-- circumstances, this can result in operations that are easier for SMT solvers
+-- to reason about. The expressions that may be pushed down are determined on a
+-- case-by-case basis in the 'IsExprBuilder' instance for 'ExprBuilder', but
+-- this control applies to all such push-down checks.
+--
+-- This option is named \"backend.push_mux_ops\".
+pushMuxOpsOption :: CFG.ConfigOption BaseBoolType
+pushMuxOpsOption = CFG.configOption BaseBoolRepr "backend.push_mux_ops"
 
+-- | The 'CFG.ConfigDesc' for 'pushMuxOpsOption'.
+pushMuxOpsDesc :: CFG.ConfigDesc
+pushMuxOpsDesc = CFG.mkOpt pushMuxOpsOption sty help (Just (ConcreteBool False))
+  where sty = CFG.boolOptSty
+        help = Just $
+          "If this option enabled, push certain ExprBuilder operations " <>
+          "(e.g., zext) down to the branches of ite expressions."
+
 newExprBuilder ::
   FloatModeRepr fm
   -- ^ Float interpretation mode (i.e., how are floats translated for the solver).
@@ -670,9 +713,11 @@
   cfg <- CFG.initialConfig 0
            [ unaryThresholdDesc
            , cacheStartSizeDesc
+           , pushMuxOpsDesc
            ]
   unarySetting       <- CFG.getOptionSetting unaryThresholdOption cfg
   cacheStartSetting  <- CFG.getOptionSetting cacheStartSizeOption cfg
+  pushMuxOpsSetting  <- CFG.getOptionSetting pushMuxOpsOption cfg
   CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg
   nonLinearOps <- newIORef 0
 
@@ -683,6 +728,7 @@
                , sbFloatReduce = True
                , sbUnaryThreshold = unarySetting
                , sbCacheStartSize = cacheStartSetting
+               , sbPushMuxOps = pushMuxOpsSetting
                , sbProgramLoc = loc_ref
                , sbExprCounter = gen
                , sbCurAllocator = storage_ref
@@ -946,6 +992,351 @@
                             }
   evalBoundVars' tbls sym e
 
+
+-- | `ExprTransformer` and the associated code implement bidirectional bitvector
+-- (BV) to/from linear integer arithmetic (LIA) transformations. This is done by
+-- replacing all BV operations with LIA operations, replacing all BV variables
+-- with LIA variables, and by replacing all BV function symbols with LIA
+-- function symbols. The reverse transformation works the same way, but in
+-- reverse. This transformation is not sound, but in practice it is useful.
+--
+-- This is used to implement `transformPredBV2LIA` and `transformSymFnLIA2BV`,
+-- which in turn are used to implement @runZ3Horn@.
+--
+-- This is highly experimental and may be unstable.
+newtype ExprTransformer t (tp1 :: BaseType) (tp2 :: BaseType) a =
+  ExprTransformer (ExceptT String (ReaderT (ExprTransformerTables t tp1 tp2) IO) a)
+  deriving (Functor, Applicative, Monad, MonadIO, MonadReader (ExprTransformerTables t tp1 tp2), MonadError String)
+
+data ExprTransformerTables t (tp1 :: BaseType) (tp2 :: BaseType) = ExprTransformerTables
+  { evalTables :: !(EvalHashTables t)
+  , transformerSubst :: !(H.BasicHashTable (ExprBoundVar t tp1) (ExprBoundVar t tp2))
+  , transformerFnSubst :: !(H.BasicHashTable (SomeExprSymFn t) (SomeExprSymFn t))
+  }
+
+runExprTransformer :: ExprTransformer t tp1 tp2 a -> ExprTransformerTables t tp1 tp2 -> IO (Either String a)
+runExprTransformer (ExprTransformer action) = runReaderT (runExceptT action)
+
+type BV2LIAExprTransformer t = ExprTransformer t (BaseBVType 64) BaseIntegerType
+type LIA2BVExprTransformer t = ExprTransformer t BaseIntegerType (BaseBVType 64)
+type HasTransformerConstraints t st fs tp1 tp2 =
+  ( KnownRepr BaseTypeRepr tp1
+  , KnownRepr BaseTypeRepr tp2
+  , ?transformCmpTp1ToTp2 :: ExprBuilder t st fs -> Expr t BaseBoolType -> Maybe (ExprTransformer t tp1 tp2 (Expr t BaseBoolType))
+  , ?transformExprTp1ToTp2 :: ExprBuilder t st fs -> Expr t tp1 -> ExprTransformer t tp1 tp2 (Expr t tp2)
+  )
+
+transformPred ::
+  forall t st fs tp1 tp2 .
+  HasTransformerConstraints t st fs tp1 tp2 =>
+  ExprBuilder t st fs ->
+  Expr t BaseBoolType ->
+  ExprTransformer t tp1 tp2 (Expr t BaseBoolType)
+transformPred sym e0 = exprTransformerCachedEval e0 $ case e0 of
+  _ | Just action <- ?transformCmpTp1ToTp2 sym e0 -> action
+
+  BoolExpr{} -> return e0
+
+  AppExpr ae -> do
+    let a = appExprApp ae
+    a' <- traverseApp
+      (\a'' -> case testEquality BaseBoolRepr (exprType a'') of
+        Just Refl -> transformPred sym a''
+        Nothing -> throwError $ "transformPred: unsupported non-boolean expression " ++ show a'')
+      a
+    if a == a' then
+      return e0
+    else
+      liftIO $ reduceApp sym bvUnary a'
+
+  NonceAppExpr ae -> do
+    case nonceExprApp ae of
+      Annotation tpr n a -> do
+        a' <- transformPred sym a
+        if a == a' then
+          return e0
+        else
+          liftIO $ sbNonceExpr sym $ Annotation tpr n a'
+      Forall v e -> do
+        quantifier <- transformVarTp1ToTp2WithCont sym v (forallPred sym)
+        -- Regenerate forallPred if e is changed by evaluation.
+        runIfChanged e (transformPred sym) e0 $ liftIO . quantifier
+      Exists v e -> do
+        quantifier <- transformVarTp1ToTp2WithCont sym v (existsPred sym)
+        -- Regenerate existsPred if e is changed by evaluation.
+        runIfChanged e (transformPred sym) e0 $ liftIO . quantifier
+      FnApp f a -> do
+        (SomeExprSymFn f') <- transformFn sym $ SomeExprSymFn f
+        (Some a') <- Ctx.fromList <$> mapM
+          (\(Some a'') ->
+            applyTp1ToTp2FunWithCont (?transformExprTp1ToTp2 sym) (transformPred sym) Some (exprType a'') a'')
+          (toListFC Some a)
+        case testEquality ((fmapFC exprType a') :> (fnReturnType f)) ((fnArgTypes f') :> (fnReturnType f')) of
+          Just Refl -> liftIO $ applySymFn sym f' a'
+          Nothing -> throwError $ "transformPred: unsupported FnApp " ++ show e0
+      _ -> throwError $ "transformPred: unsupported NonceAppExpr " ++ show e0
+
+  BoundVarExpr{} -> return e0
+
+transformFn ::
+  forall t st fs tp1 tp2 .
+  HasTransformerConstraints t st fs tp1 tp2 =>
+  ExprBuilder t st fs ->
+  SomeExprSymFn t ->
+  ExprTransformer t tp1 tp2 (SomeExprSymFn t)
+transformFn sym (SomeExprSymFn f) = do
+  inv_subst <- asks transformerFnSubst
+  case symFnInfo f of
+    UninterpFnInfo{}
+      | Just Refl <- testEquality BaseBoolRepr (fnReturnType f) -> do
+        (Some tps) <- Ctx.fromList <$> mapM
+          (\(Some tp) -> applyTp1ToTp2FunWithCont (\_ -> return knownRepr) return Some tp tp)
+          (toListFC Some $ fnArgTypes f)
+        liftIO $ mutateInsertIO inv_subst (SomeExprSymFn f) $
+          SomeExprSymFn <$> freshTotalUninterpFn sym (symFnName f) tps BaseBoolRepr
+      | otherwise -> throwError $ "transformFn: unsupported UninterpFnInfo " ++ show f
+
+    DefinedFnInfo vars e eval_fn
+      | Just Refl <- testEquality BaseBoolRepr (fnReturnType f) -> do
+        (Some vars') <- Ctx.fromList <$>
+          mapM (\(Some v) -> transformVarTp1ToTp2WithCont sym v Some) (toListFC Some vars)
+        e' <- transformPred sym e
+        liftIO $ mutateInsertIO inv_subst (SomeExprSymFn f) $
+          SomeExprSymFn <$> definedFn sym (symFnName f) vars' e' eval_fn
+      | otherwise -> throwError $ "transformFn: unsupported DefinedFnInfo " ++ show f
+
+    MatlabSolverFnInfo{} -> throwError $ "transformFn: unsupported MatlabSolverFnInfo " ++ show f
+
+exprTransformerCachedEval ::
+  Expr t tp -> ExprTransformer t tp1 tp2 (Expr t tp) -> ExprTransformer t tp1 tp2 (Expr t tp)
+exprTransformerCachedEval e action = do
+  tbls <- asks evalTables
+  cachedEval (exprTable tbls) e action
+
+transformCmpBV2LIA ::
+  ExprBuilder t st fs ->
+  Expr t BaseBoolType ->
+  Maybe (BV2LIAExprTransformer t (Expr t BaseBoolType))
+transformCmpBV2LIA sym e
+  | Just (BaseEq _ x y) <- asApp e
+  , Just Refl <- testEquality (BaseBVRepr $ knownNat @64) (exprType x) = Just $ do
+    x' <- transformExprBV2LIA sym x
+    y' <- transformExprBV2LIA sym y
+    liftIO $ intEq sym x' y'
+
+  | Just (BVUlt x y) <- asApp e
+  , Just Refl <- testEquality (BaseBVRepr $ knownNat @64) (exprType x) = Just $ do
+    x' <- transformExprBV2LIA sym x
+    y' <- transformExprBV2LIA sym y
+    liftIO $ intLt sym x' y'
+
+  | Just (BVSlt x y) <- asApp e
+  , Just Refl <- testEquality (BaseBVRepr $ knownNat @64) (exprType x) = Just $ do
+    x' <- transformExprBV2LIA sym x
+    y' <- transformExprBV2LIA sym y
+    liftIO $ intLt sym x' y'
+
+  | otherwise = Nothing
+
+transformExprBV2LIA ::
+  ExprBuilder t st fs ->
+  Expr t (BaseBVType 64) ->
+  BV2LIAExprTransformer t (Expr t BaseIntegerType)
+transformExprBV2LIA sym e
+  | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e =
+    liftIO . semiRingSum sym =<<
+      WSum.transformSum
+        SR.SemiRingIntegerRepr
+        (return . BV.asSigned (bvWidth e))
+        (transformExprBV2LIA sym)
+        semi_ring_sum
+
+  | Just semi_ring_prod <- asSemiRingProd (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e
+  , Just e' <- WSum.asProdVar semi_ring_prod =
+    transformExprBV2LIA sym e'
+
+  | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth e)) e
+  , Just e' <- WSum.asVar semi_ring_sum =
+    transformExprBV2LIA sym e'
+
+  | Just semi_ring_prod <- asSemiRingProd (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth e)) e
+  , Just e' <- WSum.asProdVar semi_ring_prod =
+    transformExprBV2LIA sym e'
+
+  | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth e)) e
+  , Just (c', e') <- WSum.asWeightedVar semi_ring_sum
+  , Just semi_ring_sum' <- asSemiRingSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e')) e'
+  , Just (c'', e'') <- WSum.asWeightedVar semi_ring_sum'
+  , Just (BaseIte _ _ c a b) <- asApp e''
+  , Just a_bv <- asBV a
+  , Just b_bv <- asBV b = do
+    x <- liftIO $ bvLit sym (bvWidth e) $ BV.xor c' $ BV.mul (bvWidth e) c'' a_bv
+    y <- liftIO $ bvLit sym (bvWidth e) $ BV.xor c' $ BV.mul (bvWidth e) c'' b_bv
+    transformExprBV2LIA sym =<< liftIO (bvIte sym c x y)
+
+  | BoundVarExpr v <- e =
+    BoundVarExpr <$> transformVarTp1ToTp2 sym v
+
+  | Just (BaseIte _ _ c x y) <- asApp e = do
+    let ?transformCmpTp1ToTp2 = transformCmpBV2LIA
+        ?transformExprTp1ToTp2 = transformExprBV2LIA
+    c' <- transformPred sym c
+    x' <- transformExprBV2LIA sym x
+    y' <- transformExprBV2LIA sym y
+    liftIO $ intIte sym c' x' y'
+
+  | Just (BVShl w x y) <- asApp e
+  , Just y_bv <- asBV y = do
+    e' <- liftIO $ bvMul sym x =<< bvLit sym w (BV.mkBV w $ 2 ^ BV.asUnsigned y_bv)
+    transformExprBV2LIA sym e'
+
+  | Just (BVLshr w x y) <- asApp e
+  , Just y_bv <- asBV y = do
+    e' <- liftIO $ bvUdiv sym x =<< bvLit sym w (BV.mkBV w $ 2 ^ BV.asUnsigned y_bv)
+    transformExprBV2LIA sym e'
+
+  | Just (BVUdiv _w x y) <- asApp e
+  , Just y_bv <- asBV y = do
+    x' <- transformExprBV2LIA sym x
+    y' <- liftIO $ intLit sym $ BV.asUnsigned y_bv
+    liftIO $ intDiv sym x' y'
+
+  | Just (BVUrem _w x y) <- asApp e
+  , Just y_bv <- asBV y = do
+    x' <- transformExprBV2LIA sym x
+    y' <- liftIO $ intLit sym $ BV.asUnsigned y_bv
+    liftIO $ intMod sym x' y'
+
+  | otherwise = throwError $ "transformExprBV2LIA: unsupported " ++ show e
+
+transformCmpLIA2BV ::
+  ExprBuilder t st fs ->
+  Expr t BaseBoolType ->
+  Maybe (LIA2BVExprTransformer t (Expr t BaseBoolType))
+transformCmpLIA2BV sym e
+  | Just (BaseEq BaseIntegerRepr x y) <- asApp e = Just $ do
+    let (x_pos, x_neg) = asPositiveNegativeWeightedSum x
+    let (y_pos, y_neg) = asPositiveNegativeWeightedSum y
+    x' <- liftIO $ semiRingSum sym $ WSum.add SR.SemiRingIntegerRepr x_pos y_neg
+    y' <- liftIO $ semiRingSum sym $ WSum.add SR.SemiRingIntegerRepr y_pos x_neg
+    x'' <- transformExprLIA2BV sym x'
+    y'' <- transformExprLIA2BV sym y'
+    liftIO $ bvEq sym x'' y''
+
+  | Just (SemiRingLe SR.OrderedSemiRingIntegerRepr x y) <- asApp e = Just $ do
+    z <- liftIO $ intSub sym x y
+    let (z_pos, z_neg) = asPositiveNegativeWeightedSum z
+    x' <- liftIO . bvSemiRingZext sym (knownNat :: NatRepr 72)
+      =<< transformExprLIA2BV sym
+      =<< liftIO (semiRingSum sym z_pos)
+    y' <- liftIO . bvSemiRingZext sym (knownNat :: NatRepr 72)
+      =<< transformExprLIA2BV sym
+      =<< liftIO (semiRingSum sym z_neg)
+    liftIO $ bvUle sym x' y'
+
+  | otherwise = Nothing
+
+asPositiveNegativeWeightedSum ::
+  Expr t BaseIntegerType ->
+  (WSum.WeightedSum (Expr t) SR.SemiRingInteger, WSum.WeightedSum (Expr t) SR.SemiRingInteger)
+asPositiveNegativeWeightedSum e = do
+  let semi_ring_sum = asWeightedSum SR.SemiRingIntegerRepr e
+  let positive_semi_ring_sum = runIdentity $ WSum.traverseCoeffs
+        (return . max 0)
+        semi_ring_sum
+  let negative_semi_ring_sum = runIdentity $ WSum.traverseCoeffs
+        (return . negate . min 0)
+        semi_ring_sum
+  (positive_semi_ring_sum, negative_semi_ring_sum)
+
+transformExprLIA2BV ::
+  ExprBuilder t st fs ->
+  Expr t BaseIntegerType ->
+  LIA2BVExprTransformer t (Expr t (BaseBVType 64))
+transformExprLIA2BV sym e
+  | Just semi_ring_sum <- asSemiRingSum SR.SemiRingIntegerRepr e =
+    liftIO . semiRingSum sym =<<
+      WSum.transformSum
+        (SR.SemiRingBVRepr SR.BVArithRepr knownNat)
+        (return . BV.mkBV knownNat)
+        (transformExprLIA2BV sym)
+        semi_ring_sum
+
+  | BoundVarExpr v <- e =
+    BoundVarExpr <$> transformVarTp1ToTp2 sym v
+
+  | Just (BaseIte _ _ c x y) <- asApp e = do
+    let ?transformCmpTp1ToTp2 = transformCmpLIA2BV
+        ?transformExprTp1ToTp2 = transformExprLIA2BV
+    c' <- transformPred sym c
+    x' <- transformExprLIA2BV sym x
+    y' <- transformExprLIA2BV sym y
+    liftIO $ bvIte sym c' x' y'
+
+  | otherwise = throwError $ "transformExprLIA2BV: unsupported " ++ show e
+
+bvSemiRingZext :: (1 <= w, 1 <= w', w + 1 <= w')
+  => ExprBuilder t st fs
+  -> NatRepr w'
+  -> Expr t (BaseBVType w)
+  -> IO (Expr t (BaseBVType w'))
+bvSemiRingZext sym w' e
+  | Just semi_ring_sum <- asSemiRingSum (SR.SemiRingBVRepr SR.BVArithRepr (bvWidth e)) e =
+    liftIO . semiRingSum sym =<<
+      WSum.transformSum
+        (SR.SemiRingBVRepr SR.BVArithRepr w')
+        (return . BV.zext w')
+        (bvZext sym w')
+        semi_ring_sum
+  | otherwise = bvZext sym w' e
+
+transformVarTp1ToTp2WithCont ::
+  forall t st fs tp tp1 tp2 a .
+  (KnownRepr BaseTypeRepr tp1, KnownRepr BaseTypeRepr tp2) =>
+  ExprBuilder t st fs ->
+  ExprBoundVar t tp ->
+  (forall tp' . ExprBoundVar t tp' -> a) ->
+  ExprTransformer t tp1 tp2 a
+transformVarTp1ToTp2WithCont sym v k = applyTp1ToTp2FunWithCont (transformVarTp1ToTp2 sym) return k (bvarType v) v
+
+transformVarTp1ToTp2 ::
+  (KnownRepr BaseTypeRepr tp1, KnownRepr BaseTypeRepr tp2) =>
+  ExprBuilder t st fs ->
+  ExprBoundVar t tp1 ->
+  ExprTransformer t tp1 tp2 (ExprBoundVar t tp2)
+transformVarTp1ToTp2 sym v = do
+  tbl <- asks transformerSubst
+  liftIO $ mutateInsertIO tbl v $ sbMakeBoundVar sym (bvarName v) knownRepr (bvarKind v) Nothing
+
+applyTp1ToTp2FunWithCont ::
+  forall t tp tp1 tp2 e a .
+  (KnownRepr BaseTypeRepr tp1, KnownRepr BaseTypeRepr tp2, Show (e tp)) =>
+  (e tp1 -> ExprTransformer t tp1 tp2 (e tp2)) ->
+  (e BaseBoolType -> ExprTransformer t tp1 tp2 (e BaseBoolType)) ->
+  (forall tp' . e tp' -> a) ->
+  BaseTypeRepr tp ->
+  e tp ->
+  ExprTransformer t tp1 tp2 a
+applyTp1ToTp2FunWithCont f g k tp e
+  | Just Refl <- testEquality (knownRepr :: BaseTypeRepr tp1) tp =
+    k <$> f e
+  | Just Refl <- testEquality BaseBoolRepr tp =
+    k <$> g e
+  | otherwise = throwError $ "applyTp1ToTp2FunWithCont: unsupported " ++ show e
+
+mutateInsertIO ::
+  (HC.HashTable h, Eq k, Hashable k) =>
+  H.IOHashTable h k v ->
+  k ->
+  IO v ->
+  IO v
+mutateInsertIO tbl k f = H.mutateIO tbl k $ \case
+  Just v -> return (Just v, v)
+  Nothing -> do
+    v <- f
+    return (Just v, v)
+
+
 -- | This attempts to lookup an entry in a symbolic array.
 --
 -- It patterns maps on the array constructor.
@@ -987,7 +1378,7 @@
   , Ctx.Empty Ctx.:> idx0 <- idx
   , Ctx.Empty Ctx.:> update_idx0 <- update_idx = do
     diff <- bvSub sym idx0 update_idx0
-    is_diff_zero <- bvEq sym diff =<< bvLit sym (bvWidth diff) (BV.zero (bvWidth diff))
+    is_diff_zero <- bvEq sym diff =<< bvZero sym (bvWidth diff)
     case asConstantPred is_diff_zero of
       Just True -> return v
       Just False -> sbConcreteLookup sym arr mcidx idx
@@ -1630,6 +2021,7 @@
 
   annotateTerm sym e =
     case e of
+      BoundVarExpr (bvarId -> n) -> return (n, e)
       NonceAppExpr (nonceExprApp -> Annotation _ n _) -> return (n, e)
       _ -> do
         let tpr = exprType e
@@ -1639,6 +2031,7 @@
 
   getAnnotation _sym e =
     case e of
+      BoundVarExpr (bvarId -> n) -> Just n
       NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n
       _ -> Nothing
 
@@ -2292,7 +2685,7 @@
 
   bvFill sym w p
     | Just True  <- asConstantPred p = bvLit sym w (BV.maxUnsigned w)
-    | Just False <- asConstantPred p = bvLit sym w (BV.zero w)
+    | Just False <- asConstantPred p = bvZero sym w
     | otherwise = sbMakeExpr sym $ BVFill w p
 
   bvIte sym c x y
@@ -2426,7 +2819,7 @@
    -- shift by more than word width returns 0
    | let (lo, _hi) = BVD.ubounds (exprAbsValue y)
    , lo >= intValue (bvWidth x)
-   = bvLit sym (bvWidth x) (BV.zero (bvWidth x))
+   = bvZero sym (bvWidth x)
 
    | Just xv <- asBV x, Just n <- asBV y
    = bvLit sym (bvWidth x) (BV.shl (bvWidth x) xv (BV.asNatural n))
@@ -2442,7 +2835,7 @@
    -- shift by more than word width returns 0
    | let (lo, _hi) = BVD.ubounds (exprAbsValue y)
    , lo >= intValue (bvWidth x)
-   = bvLit sym (bvWidth x) (BV.zero (bvWidth x))
+   = bvZero sym (bvWidth x)
 
    | Just xv <- asBV x, Just n <- asBV y
    = bvLit sym (bvWidth x) $ BV.lshr (bvWidth x) xv (BV.asNatural n)
@@ -2559,9 +2952,20 @@
       bvUnary sym $ UnaryBV.uext u w
 
     | otherwise = do
-      Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w
-      sbMakeExpr sym $ BVZext w x
+      pmo <- CFG.getOpt (sbPushMuxOps sym)
+      if | pmo
+         , Just (BaseIte _ _ c a b) <- asApp x
+         , Just a_bv <- asBV a
+         , Just b_bv <- asBV b -> do
+             Just LeqProof <- return $ isPosNat w
+             a' <- bvLit sym w $ BV.zext w a_bv
+             b' <- bvLit sym w $ BV.zext w b_bv
+             bvIte sym c a' b'
 
+         | otherwise -> do
+             Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w
+             sbMakeExpr sym $ BVZext w x
+
   bvSext sym w x
     | Just xv <- asBV x = do
       -- Add dynamic check for GHC typechecker.
@@ -2582,11 +2986,22 @@
       bvUnary sym $ UnaryBV.sext u w
 
     | otherwise = do
-      Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w
-      sbMakeExpr sym (BVSext w x)
+      pmo <- CFG.getOpt (sbPushMuxOps sym)
+      if | pmo
+         , Just (BaseIte _ _ c a b) <- asApp x
+         , Just a_bv <- asBV a
+         , Just b_bv <- asBV b -> do
+             Just LeqProof <- return $ isPosNat w
+             a' <- bvLit sym w $ BV.sext (bvWidth x) w a_bv
+             b' <- bvLit sym w $ BV.sext (bvWidth x) w b_bv
+             bvIte sym c a' b'
 
+         | otherwise -> do
+             Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w
+             sbMakeExpr sym (BVSext w x)
+
   bvXorBits sym x y
-    | x == y = bvLit sym (bvWidth x) (BV.zero (bvWidth x))  -- special case: x `xor` x = 0
+    | x == y = bvZero sym (bvWidth x)  -- special case: x `xor` x = 0
     | otherwise
     = let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)
        in semiRingAdd sym sr x y
@@ -2603,9 +3018,29 @@
     = return x -- absorption law
 
     | otherwise
-    = let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)
-       in semiRingMul sym sr x y
+    = do pmo <- CFG.getOpt (sbPushMuxOps sym)
+         if | pmo
+            , Just (BaseIte _ _ c a b) <- asApp x
+            , Just a_bv <- asBV a
+            , Just b_bv <- asBV b
+            , Just y_bv <- asBV y -> do
+                a' <- bvLit sym (bvWidth x) $ BV.and a_bv y_bv
+                b' <- bvLit sym (bvWidth x) $ BV.and b_bv y_bv
+                bvIte sym c a' b'
 
+            | pmo
+            , Just (BaseIte _ _ c a b) <- asApp y
+            , Just a_bv <- asBV a
+            , Just b_bv <- asBV b
+            , Just x_bv <- asBV x -> do
+                a' <- bvLit sym (bvWidth x) $ BV.and x_bv a_bv
+                b' <- bvLit sym (bvWidth x) $ BV.and x_bv b_bv
+                bvIte sym c a' b'
+
+            | otherwise
+            -> let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)
+                in semiRingMul sym sr x y
+
   -- XOR by the all-1 constant of the bitwise semiring.
   -- This is equivalant to negation
   bvNotBits sym x
@@ -2613,8 +3048,17 @@
     = bvLit sym (bvWidth x) $ xv `BV.xor` (BV.maxUnsigned (bvWidth x))
 
     | otherwise
-    = let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x))
-       in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x))
+    = do pmo <- CFG.getOpt (sbPushMuxOps sym)
+         if | pmo
+            , Just (BaseIte _ _ c a b) <- asApp x
+            , Just a_bv <- asBV a
+            , Just b_bv <- asBV b -> do
+                a' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) a_bv
+                b' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) b_bv
+                bvIte sym c a' b'
+            | otherwise ->
+                let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x))
+                 in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x))
 
   bvOrBits sym x y =
     case (asBV x, asBV y) of
@@ -2691,14 +3135,23 @@
 
   bvNeg sym x
     | Just xv <- asBV x = bvLit sym (bvWidth x) (BV.negate (bvWidth x) xv)
-    | otherwise =
-        do ut <- CFG.getOpt (sbUnaryThreshold sym)
-           let ?unaryThreshold = fromInteger ut
-           sbTryUnaryTerm sym
-             (do ux <- asUnaryBV sym x
-                 Just (UnaryBV.neg sym ux))
-             (do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)
-                 scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x)
+    | otherwise = do
+        pmo <- CFG.getOpt (sbPushMuxOps sym)
+        if | pmo
+           , Just (BaseIte _ _ c a b) <- asApp x
+           , Just a_bv <- asBV a
+           , Just b_bv <- asBV b -> do
+               a' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) a_bv
+               b' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) b_bv
+               bvIte sym c a' b'
+           | otherwise -> do
+               ut <- CFG.getOpt (sbUnaryThreshold sym)
+               let ?unaryThreshold = fromInteger ut
+               sbTryUnaryTerm sym
+                 (do ux <- asUnaryBV sym x
+                     Just (UnaryBV.neg sym ux))
+                 (do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)
+                     scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x)
 
   bvIsNonzero sym x
     | Just (BaseIte _ _ p t f) <- asApp x
@@ -2724,7 +3177,7 @@
             ubv
     | otherwise = do
           let w = bvWidth x
-          zro <- bvLit sym w (BV.zero w)
+          zro <- bvZero sym w
           notPred sym =<< bvEq sym x zro
 
   bvUdiv = bvBinDivOp (const BV.uquot) BVUdiv
@@ -2991,26 +3444,28 @@
      else
       sbMakeExpr sym $ ArrayMap idx_tps baseRepr new_map def_map
 
-  arrayIte sym p x y
-       -- Extract all concrete updates out.
-     | ArrayMapView mx x' <- viewArrayMap x
-     , ArrayMapView my y' <- viewArrayMap y
-     , not (AUM.null mx) || not (AUM.null my) = do
-       case exprType x of
-         BaseArrayRepr idxRepr bRepr -> do
-           let both_fn _ u v = baseTypeIte sym p u v
-               left_fn idx u = do
-                 v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx
-                 both_fn idx u v
-               right_fn idx v = do
-                 u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx
-                 both_fn idx u v
-           mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my
-           z' <- arrayIte sym p x' y'
+  arrayIte sym p x y = do
+    pmo <- CFG.getOpt (sbPushMuxOps sym)
+    if   -- Extract all concrete updates out.
+       | not pmo
+       , ArrayMapView mx x' <- viewArrayMap x
+       , ArrayMapView my y' <- viewArrayMap y
+       , not (AUM.null mx) || not (AUM.null my) -> do
+         case exprType x of
+           BaseArrayRepr idxRepr bRepr -> do
+             let both_fn _ u v = baseTypeIte sym p u v
+                 left_fn idx u = do
+                   v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx
+                   both_fn idx u v
+                 right_fn idx v = do
+                   u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx
+                   both_fn idx u v
+             mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my
+             z' <- arrayIte sym p x' y'
 
-           sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'
+             sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'
 
-     | otherwise = mkIte sym p x y
+       | otherwise -> mkIte sym p x y
 
   arrayEq sym x y
     | x == y =
@@ -3074,7 +3529,7 @@
 
   predToBV sym p w
     | Just b <- asConstantPred p =
-        if b then bvLit sym w (BV.one w) else bvLit sym w (BV.zero w)
+        if b then bvOne sym w else bvZero sym w
     | otherwise =
        case testNatCases w (knownNat @1) of
          NatCaseEQ   -> sbMakeExpr sym (BVFill (knownNat @1) p)
@@ -4076,6 +4531,48 @@
         , fnTable  = fn_tbl
         }
     evalBoundVars' tbls sym e
+
+  transformPredBV2LIA sym exprs = do
+    expr_tbl <- stToIO PH.new
+    fn_tbl  <- stToIO PH.new
+    let tbls = EvalHashTables
+          { exprTable = expr_tbl
+          , fnTable  = fn_tbl
+          }
+    subst <- H.new
+    fn_subst <- H.new
+    let transformer_tbls = ExprTransformerTables
+          { evalTables = tbls
+          , transformerSubst = subst
+          , transformerFnSubst = fn_subst
+          }
+    let ?transformCmpTp1ToTp2 = transformCmpBV2LIA
+        ?transformExprTp1ToTp2 = transformExprBV2LIA
+    lia_exprs <- either fail return =<<
+      runExprTransformer (mapM (transformPred sym) exprs) transformer_tbls
+    bv_to_lia_fn_subst <- Map.fromList <$>
+      map (\(SomeExprSymFn f, SomeExprSymFn g) -> (SomeSymFn f, SomeSymFn g)) <$>
+      H.toList fn_subst
+    return (lia_exprs, bv_to_lia_fn_subst)
+
+  transformSymFnLIA2BV sym (SomeSymFn fn) = do
+    expr_tbl <- stToIO PH.new
+    fn_tbl  <- stToIO PH.new
+    let tbls = EvalHashTables
+          { exprTable = expr_tbl
+          , fnTable  = fn_tbl
+          }
+    subst <- H.new
+    fn_subst <- H.new
+    let transformer_tbls = ExprTransformerTables
+          { evalTables = tbls
+          , transformerSubst = subst
+          , transformerFnSubst = fn_subst
+          }
+    let ?transformCmpTp1ToTp2 = transformCmpLIA2BV
+        ?transformExprTp1ToTp2 = transformExprLIA2BV
+    either fail (\(SomeExprSymFn fn') -> return $ SomeSymFn fn') =<<
+      runExprTransformer (transformFn sym $ SomeExprSymFn fn) transformer_tbls
 
 
 instance IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs)
diff --git a/src/What4/Expr/MATLAB.hs b/src/What4/Expr/MATLAB.hs
--- a/src/What4/Expr/MATLAB.hs
+++ b/src/What4/Expr/MATLAB.hs
@@ -106,7 +106,7 @@
 clampedIntMul sym x y = do
   let w = bvWidth x
   (hi,lo) <- signedWideMultiplyBV sym x y
-  zro    <- bvLit sym w (BV.zero w)
+  zro    <- bvZero sym w
   ones   <- maxUnsignedBV sym w
   ok_pos <- join $ andPred sym <$> (notPred sym =<< bvIsNeg sym lo)
                               <*> bvEq sym hi zro
@@ -178,7 +178,7 @@
        sym
        no_underflow
        (bvSub sym x y) -- Perform subtraction if y >= x
-       (bvLit sym w (BV.zero w)) -- Otherwise return min int
+       (bvZero sym w) -- Otherwise return min int
 
 clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
                => sym
diff --git a/src/What4/Interface.hs b/src/What4/Interface.hs
--- a/src/What4/Interface.hs
+++ b/src/What4/Interface.hs
@@ -156,6 +156,10 @@
   , SymEncoder(..)
 
     -- * Utility combinators
+    -- ** Bitvector operations
+  , bvZero
+  , bvOne
+
     -- ** Boolean operations
   , backendPred
   , andAllOf
@@ -205,6 +209,7 @@
 import           Data.Coerce (coerce)
 import           Data.Foldable
 import           Data.Kind ( Type )
+import           Data.Map.Strict (Map)
 import qualified Data.Map as Map
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Context as Ctx
@@ -691,7 +696,8 @@
   getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
 
   -- | Project the original, unannotated term from an annotated term.
-  --   This returns 'Nothing' for terms that do not have annotations.
+  --   This returns 'Nothing' for terms that do not have annotations,
+  --   or for terms that cannot be separated from their annotations.
   getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp)
 
   ----------------------------------------------------------------------
@@ -943,7 +949,7 @@
 
   -- | Return true if bitvector is negative.
   bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
-  bvIsNeg sym x = bvSlt sym x =<< bvLit sym (bvWidth x) (BV.zero (bvWidth x))
+  bvIsNeg sym x = bvSlt sym x =<< bvZero sym (bvWidth x)
 
   -- | If-then-else applied to bitvectors.
   bvIte :: (1 <= w)
@@ -1691,7 +1697,7 @@
       -- Handle case where i < 0
       min_sym <- intLit sym 0
       is_lt <- intLt sym i min_sym
-      iteM bvIte sym is_lt (bvLit sym w (BV.zero w)) $ do
+      iteM bvIte sym is_lt (bvZero sym w) $ do
         -- Handle case where i > maxUnsigned w
         let max_val = maxUnsigned w
             max_val_bv = BV.maxUnsigned w
@@ -1741,7 +1747,7 @@
   intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
   intToUInt sym e w = do
     p <- bvIsNeg sym e
-    iteM bvIte sym p (bvLit sym w (BV.zero w)) (uintSetWidth sym e w)
+    iteM bvIte sym p (bvZero sym w) (uintSetWidth sym e w)
 
   -- | Convert an unsigned bitvector to the nearest signed bitvector with
   -- the given width (clamp on overflow).
@@ -2729,6 +2735,12 @@
 
 data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)
 
+instance IsSymFn (SymFn sym) => Eq (SomeSymFn sym) where
+  (SomeSymFn fn1) == (SomeSymFn fn2) = isJust $ fnTestEquality fn1 fn2
+
+instance IsSymFn (SymFn sym) => Ord (SomeSymFn sym) where
+  compare (SomeSymFn fn1) (SomeSymFn fn2) = toOrdering $ fnCompare fn1 fn2
+
 -- | Wrapper for `SymFn` that concatenates the arguments and the return types.
 --
 -- This is useful for implementing `TestEquality` and `OrdF` instances for
@@ -2968,6 +2980,21 @@
     SymExpr sym tp ->
     IO (SymExpr sym tp)
 
+  -- | Transform a BV predicate into an LIA predicate by replacing all bitvector
+  -- (BV) operations with LIA operations, and replacing all BV variables with
+  -- LIA variables. This transformation is not sound, but in practice it is
+  -- useful. It returns the transformed predicate and a map from the original
+  -- uninterpreted function symbols to the trnasformed uninterpreted function
+  -- symbols.
+  transformPredBV2LIA :: sym -> [Pred sym] -> IO ([Pred sym], Map (SomeSymFn sym) (SomeSymFn sym))
+
+  -- | Transform a LIA defined boolean function into a BV defined boolean
+  -- function by replacing all LIA operations with BV operations. Currently, the
+  -- BV width for function parameters is set to 64, and for operations is set to
+  -- 72.
+  transformSymFnLIA2BV :: sym -> SomeSymFn sym -> IO (SomeSymFn sym)
+
+
 -- | This returns true if the value corresponds to a concrete value.
 baseIsConcrete :: forall e bt
                 . IsExpr e
@@ -3004,7 +3031,7 @@
   case bt of
     BaseBoolRepr    -> return $! falsePred sym
     BaseIntegerRepr -> intLit sym 0
-    BaseBVRepr w    -> bvLit sym w (BV.zero w)
+    BaseBVRepr w    -> bvZero sym w
     BaseRealRepr    -> return $! realZero sym
     BaseFloatRepr fpp -> floatPZero sym fpp
     BaseComplexRepr -> mkComplexLit sym (0 :+ 0)
@@ -3271,3 +3298,17 @@
 zeroStatistics :: Statistics
 zeroStatistics = Statistics { statAllocs = 0
                             , statNonLinearOps = 0 }
+
+----------------------------------------------------------------------
+-- Bitvector utilities
+
+-- | An alias for 'minUnsignedBv'.
+--
+-- Useful in contexts where you want to convey the zero-ness of the value more
+-- than its minimality.
+bvZero :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)
+bvZero = minUnsignedBV
+
+-- | A bitvector that is all zeroes except the LSB, which is one.
+bvOne :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)
+bvOne sym w = bvLit sym w (BV.one w)
diff --git a/src/What4/Protocol/SMTLib2.hs b/src/What4/Protocol/SMTLib2.hs
--- a/src/What4/Protocol/SMTLib2.hs
+++ b/src/What4/Protocol/SMTLib2.hs
@@ -101,16 +101,18 @@
 
 import           Control.Applicative
 import           Control.Exception
-import           Control.Monad (forM, forM_, replicateM_, unless, when)
+import           Control.Monad (forM, replicateM_, unless, when)
 import           Control.Monad.IO.Class (MonadIO(..))
 import           Control.Monad.Except (MonadError(..), ExceptT, runExceptT)
 import           Control.Monad.Reader (MonadReader(..), ReaderT(..), asks)
 import qualified Data.Bimap as Bimap
 import qualified Data.BitVector.Sized as BV
 import           Data.Char (digitToInt, isAscii)
+import           Data.Foldable
 import           Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
 import           Data.IORef
+import qualified Data.List as List
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Monoid
@@ -151,6 +153,7 @@
 import qualified What4.Expr.Builder as B
 import           What4.Expr.GroundEval
 import qualified What4.Interface as I
+import           What4.Panic
 import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import           What4.Protocol.ReadDecimal
@@ -984,7 +987,7 @@
       let let_env = HashMap.fromList $ zip nms $ map (mapSome $ I.varExpr sym) vars
       proc_res <- runProcessor (ProcessorEnv { procSym = sym, procLetEnv = let_env }) $ parseExpr sym body_sexp
       Some body_expr <- either fail return proc_res
-      I.SomeSymFn <$> I.definedFn sym (I.safeSymbol $ Text.unpack nm) vars_assign body_expr I.NeverUnfold
+      I.SomeSymFn <$> I.definedFn sym (I.safeSymbol $ Text.unpack nm) vars_assign body_expr I.AlwaysUnfold
 
 parseVar :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, Some (I.BoundVar sym))
 parseVar sym sexp = case sexp of
@@ -1065,7 +1068,16 @@
       Op sym
 
 data Assoc = RightAssoc | LeftAssoc
+  deriving (Eq, Ord, Show)
 
+opAssoc :: Op sym -> Maybe Assoc
+opAssoc = \case
+  Op1{} -> Nothing
+  Op2 _ assoc _ -> assoc
+  BVOp1{} -> Nothing
+  BVOp2 assoc _ -> assoc
+  BVComp2{} -> Nothing
+
 newtype Processor sym a = Processor (ExceptT String (ReaderT (ProcessorEnv sym) IO) a)
   deriving (Functor, Applicative, Monad, MonadIO, MonadError String, MonadReader (ProcessorEnv sym))
 
@@ -1168,7 +1180,44 @@
     BVProof{} <- getBVProof arg1_expr
     BVProof{} <- getBVProof arg2_expr
     liftIO $ Some <$> I.bvConcat sym arg1_expr arg2_expr
+  SApp [SApp ["_", "extract", i_sexp, j_sexp], arg]
+    | Just i <- parseIntSolverValue i_sexp
+    , Just j <- parseIntSolverValue j_sexp -> do
+      let n = i - j + 1
+      Some j_repr <- return $ mkNatRepr $ fromIntegral j
+      Some n_repr <- return $ mkNatRepr $ fromIntegral n
+      Some arg_expr <- parseExpr sym arg
+      BVProof w_repr <- getBVProof arg_expr
+      case (isPosNat n_repr, testLeq (addNat j_repr n_repr) w_repr) of
+        (Just LeqProof, Just LeqProof) ->
+          liftIO $ Some <$> I.bvSelect sym j_repr n_repr arg_expr
+        _ -> throwError ""
   SApp ((SAtom operator) : operands) -> case HashMap.lookup operator (opTable @sym) of
+    -- Sometimes, binary operators can be applied to more than two operands,
+    -- e.g., (+ 1 2 3 4). We want to uniformly represent binary operators such
+    -- that they are always applied to two operands, so this case converts the
+    -- expression above to:
+    --
+    -- - (+ (+ (+ 1 2) 3) 4) (if + is left-associative)
+    -- - (+ 1 (+ 2 (+ 3 4))) (if + is right-associative)
+    --
+    -- We then call `parseExpr` and recurse, which will reach one of the cases
+    -- below.
+    Just op
+      | Just LeftAssoc <- opAssoc op
+      , op1:op2:op3:ops <- operands ->
+          parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) op1 (op2:op3:ops)
+
+        -- For right-associative operators, we could alternatively call
+        -- init/last on the list of operands and call foldr on the results. The
+        -- downside, however, is that init/last are partial functions. To avoid
+        -- this partiality, we instead match on `reverse operands` and call
+        -- foldl on the results (with the order of acc/arg swapped). This
+        -- achieves the same end result and maintains the same asymptotic
+        -- complexity as using init/tail.
+      | Just RightAssoc <- opAssoc op
+      , op1:op2:op3:ops <- List.reverse operands ->
+          parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, arg, acc]) op1 (op2:op3:ops)
     Just (Op1 arg_types fn) -> do
       args <- mapM (parseExpr sym) operands
       exprAssignment arg_types args >>= \case
@@ -1209,6 +1258,7 @@
                                        (show n)
     _ -> throwError ""
   _ -> throwError ""
+
 -- | Verify a list of arguments has a single argument and
 -- return it, else raise an error.
 readOneArg ::
@@ -1333,8 +1383,10 @@
           AckUnsat   -> Just $ Unsat ()
           AckUnknown -> Just Unknown
           _ -> Nothing
-    in getLimitedSolverResponse "sat result" satRsp s
-       (head $ reverse $ checkCommands p)
+        cmd = case reverse $ checkCommands p of
+                cmd':_ -> cmd'
+                []     -> panic "smtSatResult" ["Empty list of checkCommands"]
+    in getLimitedSolverResponse "sat result" satRsp s cmd
 
   smtUnsatAssumptionsResult p s =
     let unsatAssumpRsp = \case
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
@@ -829,13 +829,15 @@
 cacheValueFn conn n lifetime value = cacheValue conn lifetime $ \entry ->
   stToIO $ PH.insert (symFnCache entry) n value
 
+-- | Construct a function/name bimap. Each function is associated with its
+-- cached name if there is one, otherwise with its original name.
 cacheLookupFnNameBimap :: WriterConn t h -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
 cacheLookupFnNameBimap conn fns = Bimap.fromList <$> mapM
   (\some_fn@(SomeExprSymFn fn) -> do
     maybe_smt_sym_fn <- cacheLookupFn conn $ symFnId fn
-    case maybe_smt_sym_fn of
-      Just (SMTSymFn nm _ _) -> return (some_fn, nm)
-      Nothing -> fail $ "Could not find function in cache: " ++ show fn)
+    return $ case maybe_smt_sym_fn of
+      Just (SMTSymFn nm _ _) -> (some_fn, nm)
+      Nothing -> (some_fn, solverSymbolAsText $ symFnName fn))
   fns
 
 -- | Run state with handle.
diff --git a/src/What4/Solver.hs b/src/What4/Solver.hs
--- a/src/What4/Solver.hs
+++ b/src/What4/Solver.hs
@@ -32,6 +32,16 @@
   , runExternalABCInOverride
   , writeABCSMT2File
 
+    -- * Bitwuzla
+  , Bitwuzla(..)
+  , bitwuzlaAdapter
+  , bitwuzlaPath
+  , bitwuzlaTimeout
+  , runBitwuzlaInOverride
+  , withBitwuzla
+  , bitwuzlaOptions
+  , bitwuzlaFeatures
+
     -- * Boolector
   , Boolector(..)
   , boolectorAdapter
@@ -107,6 +117,7 @@
   ) where
 
 import           What4.Solver.Adapter
+import           What4.Solver.Bitwuzla
 import           What4.Solver.Boolector
 import           What4.Solver.CVC4
 import           What4.Solver.CVC5
diff --git a/src/What4/Solver/Bitwuzla.hs b/src/What4/Solver/Bitwuzla.hs
new file mode 100644
--- /dev/null
+++ b/src/What4/Solver/Bitwuzla.hs
@@ -0,0 +1,158 @@
+------------------------------------------------------------------------
+-- |
+-- Module           : What4.Solver.Bitwuzla
+-- Description      : Interface for running Bitwuzla
+-- Copyright        : (c) Galois, Inc 2014-2023
+-- License          : BSD3
+-- Maintainer       : Ryan Scott <rscott@galois.com>
+-- Stability        : provisional
+--
+-- This module provides an interface for running Bitwuzla and parsing
+-- the results back.
+------------------------------------------------------------------------
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+module What4.Solver.Bitwuzla
+  ( Bitwuzla(..)
+  , bitwuzlaPath
+  , bitwuzlaTimeout
+  , bitwuzlaOptions
+  , bitwuzlaAdapter
+  , runBitwuzlaInOverride
+  , withBitwuzla
+  , bitwuzlaFeatures
+  ) where
+
+import           Control.Monad
+import           Data.Bits ( (.|.) )
+
+import           What4.BaseTypes
+import           What4.Concrete
+import           What4.Config
+import           What4.Expr.Builder
+import           What4.Expr.GroundEval
+import           What4.Interface
+import           What4.ProblemFeatures
+import           What4.Protocol.Online
+import qualified What4.Protocol.SMTLib2 as SMT2
+import qualified What4.Protocol.SMTLib2.Syntax as Syntax
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
+import           What4.SatResult
+import           What4.Solver.Adapter
+import           What4.Utils.Process
+
+data Bitwuzla = Bitwuzla deriving Show
+
+-- | Path to bitwuzla
+bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
+bitwuzlaPath = configOption knownRepr "solver.bitwuzla.path"
+
+-- | Per-check timeout, in milliseconds (zero is none)
+bitwuzlaTimeout :: ConfigOption BaseIntegerType
+bitwuzlaTimeout = configOption knownRepr "solver.bitwuzla.timeout"
+
+-- | Control strict parsing for Bitwuzla solver responses (defaults
+-- to solver.strict-parsing option setting).
+bitwuzlaStrictParsing :: ConfigOption BaseBoolType
+bitwuzlaStrictParsing = configOption knownRepr "solver.bitwuzla.strict_parsing"
+
+bitwuzlaOptions :: [ConfigDesc]
+bitwuzlaOptions =
+  let bpOpt co = mkOpt
+                 co
+                 executablePathOptSty
+                 (Just "Path to bitwuzla executable")
+                 (Just (ConcreteString "bitwuzla"))
+      mkTmo co = mkOpt co
+                 integerOptSty
+                 (Just "Per-check timeout in milliseconds (zero is none)")
+                 (Just (ConcreteInteger 0))
+      bp = bpOpt bitwuzlaPath
+  in [ bp
+     , mkTmo bitwuzlaTimeout
+     , copyOpt (const $ configOptionText bitwuzlaStrictParsing) strictSMTParseOpt
+     ] <> SMT2.smtlib2Options
+
+bitwuzlaAdapter :: SolverAdapter st
+bitwuzlaAdapter =
+  SolverAdapter
+  { solver_adapter_name = "bitwuzla"
+  , solver_adapter_config_options = bitwuzlaOptions
+  , solver_adapter_check_sat = runBitwuzlaInOverride
+  , solver_adapter_write_smt2 =
+      SMT2.writeDefaultSMT2 () "Bitwuzla" defaultWriteSMTLIB2Features
+      (Just bitwuzlaStrictParsing)
+  }
+
+instance SMT2.SMTLib2Tweaks Bitwuzla where
+  smtlib2tweaks = Bitwuzla
+
+runBitwuzlaInOverride
+  :: ExprBuilder t st fs
+  -> LogData
+  -> [BoolExpr t]
+  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
+  -> IO a
+runBitwuzlaInOverride =
+  SMT2.runSolverInOverride Bitwuzla SMT2.nullAcknowledgementAction
+  bitwuzlaFeatures (Just bitwuzlaStrictParsing)
+
+-- | Run Bitwuzla in a session. Bitwuzla will be configured to produce models, but
+-- otherwise left with the default configuration.
+withBitwuzla
+  :: ExprBuilder t st fs
+  -> FilePath
+    -- ^ Path to Bitwuzla executable
+  -> LogData
+  -> (SMT2.Session t Bitwuzla -> IO a)
+    -- ^ Action to run
+  -> IO a
+withBitwuzla = SMT2.withSolver Bitwuzla SMT2.nullAcknowledgementAction
+               bitwuzlaFeatures (Just bitwuzlaStrictParsing)
+
+bitwuzlaFeatures :: ProblemFeatures
+bitwuzlaFeatures = useBitvectors
+               .|. useFloatingPoint
+               .|. useQuantifiers
+               .|. useSymbolicArrays
+               .|. useUninterpFunctions
+               .|. useUnsatCores
+               .|. useUnsatAssumptions
+
+instance SMT2.SMTLib2GenericSolver Bitwuzla where
+  defaultSolverPath _ = findSolverPath bitwuzlaPath . getConfiguration
+  defaultSolverArgs _ sym = do
+    let cfg = getConfiguration sym
+    timeout <- getOption =<< getOptionSetting bitwuzlaTimeout cfg
+    let extraOpts = case timeout of
+                      Just (ConcreteInteger n) | n > 0 -> ["-t", show n]
+                      _ -> []
+    return $ ["--lang", "smt2"] ++ extraOpts
+  defaultFeatures _ = bitwuzlaFeatures
+  setDefaultLogicAndOptions writer = do
+    SMT2.setLogic writer Syntax.allLogic
+    SMT2.setProduceModels writer True
+
+setInteractiveLogicAndOptions ::
+  SMT2.SMTLib2Tweaks a =>
+  SMT2.WriterConn t (SMT2.Writer a) ->
+  IO ()
+setInteractiveLogicAndOptions writer = do
+    SMT2.setOption writer "print-success"  "true"
+    SMT2.setOption writer "produce-models" "true"
+    SMT2.setOption writer "global-declarations" "true"
+    when (SMT2.supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
+      SMT2.setOption writer "produce-unsat-cores" "true"
+    SMT2.setLogic writer Syntax.allLogic
+
+instance OnlineSolver (SMT2.Writer Bitwuzla) where
+  startSolverProcess feat mbIOh sym = do
+    timeout <- SolverGoalTimeout <$>
+               (getOpt =<< getOptionSetting bitwuzlaTimeout (getConfiguration sym))
+    SMT2.startSolver Bitwuzla SMT2.smtAckResult
+                            setInteractiveLogicAndOptions
+                            timeout
+                            feat
+                            (Just bitwuzlaStrictParsing) mbIOh sym
+  shutdownSolverProcess = SMT2.shutdownSolver Bitwuzla
diff --git a/src/What4/Solver/Z3.hs b/src/What4/Solver/Z3.hs
--- a/src/What4/Solver/Z3.hs
+++ b/src/What4/Solver/Z3.hs
@@ -12,7 +12,9 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GADTs #-}
@@ -36,12 +38,15 @@
 import qualified Data.Bimap as Bimap
 import           Data.Bits
 import           Data.Foldable
+import           Data.Map.Strict (Map)
+import qualified Data.Map as Map
 import           Data.String
 import           Data.Text (Text)
 import qualified Data.Text as T
 import           System.IO
 
 import           Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Some
 import           What4.BaseTypes
 import           What4.Concrete
@@ -248,14 +253,32 @@
 --
 -- CHCs are represented as pure SMT-LIB2 implications. For more information, see
 -- the [Z3 guide](https://microsoft.github.io/z3guide/docs/fixedpoints/intro/).
+--
+-- There are two ways to solve the CHCs: either by directly solving the problem
+-- as is, or by transforming the problem into a set of linear integer arithmetic
+-- (LIA) CHCs and solving that instead. The latter is done by replacing all
+-- bitvector (BV) operations with LIA operations, and replacing all BV variables
+-- with LIA variables. This transformation is not sound, but in practice it is a
+-- useful heuristic. Then the result is transformed back into a BV result, and
+-- checked for satisfiability. The satisfiability check is necessary because the
+-- transformation is not sound, so LIA solution may not be a solution to the BV
+-- CHCs.
 runZ3Horn ::
+  forall sym t st fs .
   sym ~ ExprBuilder t st fs =>
   sym ->
+  Bool {- transform the BV CHCs into LIA CHCs -} ->
   LogData ->
   [SomeSymFn sym] ->
   [BoolExpr t] ->
   IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
-runZ3Horn sym log_data inv_fns horn_clauses = do
+runZ3Horn sym do_bv_to_lia_transform log_data inv_fns horn_clauses = do
+  (lia_inv_fns, lia_horn_clauses, bv_to_lia_fn_subst) <- transformHornClausesForZ3
+    sym
+    do_bv_to_lia_transform
+    inv_fns
+    horn_clauses
+
   logSolverEvent sym
     (SolverStartSATQuery $ SolverStartSATQueryRec
       { satQuerySolverName = show Z3
@@ -263,9 +286,10 @@
       })
 
   path <- SMT2.defaultSolverPath Z3 sym
-  withZ3 sym path (log_data { logVerbosity = 2 }) $ \session -> do
-    writeHornProblem sym (SMT2.sessionWriter session) inv_fns horn_clauses
-    result <- RSP.getLimitedSolverResponse "check-sat"
+  get_value_result <- withZ3 sym path (log_data { logVerbosity = 2 }) $ \session -> do
+    writeHornProblem sym (SMT2.sessionWriter session) lia_inv_fns lia_horn_clauses
+
+    check_sat_result <- RSP.getLimitedSolverResponse "check-sat"
       (\case
         RSP.AckSat -> Just $ Sat ()
         RSP.AckUnsat -> Just $ Unsat ()
@@ -276,7 +300,7 @@
 
     logSolverEvent sym
       (SolverEndSATQuery $ SolverEndSATQueryRec
-        { satQueryResult = result
+        { satQueryResult = check_sat_result
         , satQueryError = Nothing
         })
 
@@ -288,18 +312,59 @@
             _ -> Nothing)
           (SMT2.sessionWriter session)
           (Syntax.getValue [])
-        SMT2.parseFnValues sym (SMT2.sessionWriter session) inv_fns sexp)
+        SMT2.parseFnValues sym (SMT2.sessionWriter session) lia_inv_fns sexp)
       return
-      result
+      check_sat_result
 
+  let transform_result_lia_to_bv ::
+        SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) () ->
+        IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
+      transform_result_lia_to_bv = \case
+        Sat lia_defined_fns -> do
+          defined_inv_fns <- MapF.fromList <$> mapM
+            (\(SomeSymFn fn) ->
+              if| Just (SomeSymFn lia_fn) <- Map.lookup (SomeSymFn fn) bv_to_lia_fn_subst
+                , Just (SymFnWrapper lia_defined_fn) <- MapF.lookup (SymFnWrapper lia_fn) lia_defined_fns -> do
+                  some_defined_fn <- transformSymFnLIA2BV sym $ SomeSymFn lia_defined_fn
+                  case some_defined_fn of
+                    SomeSymFn defined_fn
+                      | Just Refl <- testEquality (fnArgTypes fn) (fnArgTypes defined_fn)
+                      , Just Refl <- testEquality (fnReturnType fn) (fnReturnType defined_fn) ->
+                        return $ MapF.Pair (SymFnWrapper fn) (SymFnWrapper defined_fn)
+                    _ -> fail $ "runZ3Horn: function type mismatch in solver result: " ++ show fn
+                | otherwise -> fail $ "runZ3Horn: function not found in solver result: " ++ show fn)
+            inv_fns
+
+          all_unsat <- and <$> mapM
+            (\clause -> do
+              defined_clause <- notPred sym =<< substituteSymFns sym defined_inv_fns clause
+              runZ3InOverride sym (log_data { logVerbosity = 2 }) [defined_clause] $ return . isUnsat)
+            horn_clauses
+
+          return $ if all_unsat then Sat defined_inv_fns else Unknown
+
+        _ -> return Unknown
+
+  if do_bv_to_lia_transform then
+    transform_result_lia_to_bv get_value_result
+  else
+    return get_value_result
+
 writeZ3HornSMT2File ::
   sym ~ ExprBuilder t st fs =>
   sym ->
+  Bool {- transform the BV CHCs into LIA CHCs -} ->
   Handle ->
   [SomeSymFn sym] ->
   [BoolExpr t] ->
   IO ()
-writeZ3HornSMT2File sym h inv_fns horn_clauses = do
+writeZ3HornSMT2File sym do_bv_to_lia_transform h inv_fns horn_clauses = do
+  (lia_inv_fns, lia_horn_clauses, _bv_to_lia_fn_subst) <- transformHornClausesForZ3
+    sym
+    do_bv_to_lia_transform
+    inv_fns
+    horn_clauses
+
   writer <- SMT2.defaultFileWriter
     Z3
     (show Z3)
@@ -308,8 +373,22 @@
     sym
     h
   SMT2.setDefaultLogicAndOptions writer
-  writeHornProblem sym writer inv_fns horn_clauses
+  writeHornProblem sym writer lia_inv_fns lia_horn_clauses
   SMT2.writeExit writer
+
+transformHornClausesForZ3 ::
+  sym ~ ExprBuilder t st fs =>
+  sym ->
+  Bool ->
+  [SomeSymFn sym] ->
+  [BoolExpr t] ->
+  IO ([SomeSymFn sym], [BoolExpr t], Map (SomeSymFn sym) (SomeSymFn sym))
+transformHornClausesForZ3 sym do_bv_to_lia_transform inv_fns horn_clauses =
+  if do_bv_to_lia_transform then do
+    (lia_horn_clauses, bv_to_lia_fn_subst) <- transformPredBV2LIA sym horn_clauses
+    let lia_inv_fns = Map.elems bv_to_lia_fn_subst
+    return (lia_inv_fns, lia_horn_clauses, bv_to_lia_fn_subst)
+  else return (inv_fns, horn_clauses, Map.empty)
 
 writeHornProblem ::
   sym ~ ExprBuilder t st fs =>
diff --git a/test/AdapterTest.hs b/test/AdapterTest.hs
--- a/test/AdapterTest.hs
+++ b/test/AdapterTest.hs
@@ -33,7 +33,9 @@
 
 import           What4.Config
 import           What4.Expr
+import           What4.Expr.Builder ( asApp, pushMuxOpsOption )
 import           What4.Interface
+import           What4.Panic
 import           What4.Protocol.SMTLib2.Response ( strictSMTParsing )
 import           What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) )
 import           What4.Protocol.VerilogWriter
@@ -45,6 +47,7 @@
   , cvc5Adapter
   , yicesAdapter
   , z3Adapter
+  , bitwuzlaAdapter
   , boolectorAdapter
   , externalABCAdapter
 #ifdef TEST_STP
@@ -85,6 +88,7 @@
   [
     testGroup "deprecated configs" (deprecatedConfigTests adapters)
   , testGroup "strict parsing config" (strictParseConfigTests adapters)
+  , testGroup "push mux ops config" (pushMuxOpsConfigTests adapters)
   ]
   where
     wantOptSetFailure withText res = case res of
@@ -222,7 +226,50 @@
               ]
       in fmap mkPCTest adaptrs
 
+    pushMuxOpsConfigTests adaptrs =
+      let -- A basic test that ensures that pushMuxOps actually takes effect
+          -- when enabled or disabled.
+          mkPushZextMuxTest ::
+            forall a.
+            Bool ->
+            (forall t. Expr t (BaseBVType 64) -> IO a) ->
+            IO a
+          mkPushZextMuxTest pushMuxOpsVal k =
+            withAdapters adaptrs $ \sym -> do
+              pmo <- getOptionSetting pushMuxOpsOption (getConfiguration sym)
+              show <$> setOpt pmo pushMuxOpsVal >>= (@?= "[]")
+              let w = knownNat @32
+              a <- bvLit sym w $ mkBV w 27
+              b <- bvLit sym w $ mkBV w 42
+              c <- freshConstant sym (safeSymbol "c") BaseBoolRepr
+              ite <- bvIte sym c a b
+              zextIte <- bvZext sym (knownNat @64) ite
+              k zextIte
+      in [ testCase "enable pushMuxOps" $
+           mkPushZextMuxTest True $ \zextIte ->
+           case asApp zextIte of
+             Just (BaseIte {}) -> pure ()
+             _ -> assertFailure $ unlines
+                    [ "zext not pushed down through ite"
+                    , show $ printSymExpr zextIte
+                    ]
+
+         , testCase "disable pushMuxOps" $
+           mkPushZextMuxTest False $ \zextIte ->
+           case asApp zextIte of
+             Just (BVZext {}) -> pure ()
+             _ -> assertFailure $ unlines
+                    [ "zext should be at the head of the application"
+                    , show $ printSymExpr zextIte
+                    ]
+         ]
+
     deprecatedConfigTests adaptrs =
+      let firstAdapter adptrs =
+            case adptrs of
+              adptr:_ -> adptr
+              [] -> panic "deprecatedConfigTests" ["Empty list of adapters"]
+      in
       [
 
         testCaseSteps "deprecated default_solver is equivalent to solver.default" $
@@ -257,7 +304,7 @@
 
           step "Update the value via regular (text identification)"
           res2 <- try $ setUnicodeOpt settera $
-                  pack $ solver_adapter_name $ head adaptrs
+                  pack $ solver_adapter_name $ firstAdapter adaptrs
           case res2 of
             Right warns -> fmap show warns @?= []
             Left (SomeException e) -> assertFailure $ show e
@@ -282,7 +329,7 @@
 
           step "Reset to original value"
           res4 <- try $ setOpt settera' $
-                  pack $ solver_adapter_name $ head adaptrs
+                  pack $ solver_adapter_name $ firstAdapter adaptrs
           case res4 of
             Right warns -> fmap show warns @?= []
             Left (SomeException e) -> assertFailure $ show e
@@ -540,7 +587,7 @@
 
 nonlinearRealTest :: SolverAdapter EmptyExprBuilderState -> TestTree
 nonlinearRealTest adpt =
-  let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]
+  let wrap = if solver_adapter_name adpt `elem` [ "ABC", "bitwuzla", "boolector", "stp" ]
              then expectFailBecause
                   (solver_adapter_name adpt
                    <> " does not support this type of linear arithmetic term")
diff --git a/test/ConfigTest.hs b/test/ConfigTest.hs
--- a/test/ConfigTest.hs
+++ b/test/ConfigTest.hs
@@ -471,10 +471,12 @@
     withChecklist "builtins" $ do
       cfg <- initialConfig 0 []
       help <- configHelp "" cfg
+      let nonEmptyOr :: (a -> b) -> b -> [a] -> b
+          nonEmptyOr f = foldr (\h _ -> f h)
       help `checkValues`
         (Empty
         :> Val "num" length 1
-        :> Val "verbosity" (L.isInfixOf "verbosity =" . show . head) True
+        :> Val "verbosity" (nonEmptyOr (L.isInfixOf "verbosity =" . show) False) True
         )
 
 
diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs
--- a/test/ExprBuilderSMTLib2.hs
+++ b/test/ExprBuilderSMTLib2.hs
@@ -1068,7 +1068,7 @@
     let idx = Ctx.Empty Ctx.:> idxInt
     let arrLookup = arrayLookup sym arr idx
     elt <- arrLookup
-    bvZero <- bvLit sym w (BV.zero w)
+    bvZero <- bvZero sym w
     p <- bvEq sym elt bvZero
 
     checkSatisfiableWithModel solver "test" p $ \case
@@ -1133,7 +1133,7 @@
     e1A <- freshConstant sym (userSymbol' "x1") (BaseBVRepr w)
     let e1A' = unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e1A
     unsignedBVBounds e1A' @?= Just (2, 2)
-    e1B <- bvAdd sym e1A' =<< bvLit sym w (BV.one w)
+    e1B <- bvAdd sym e1A' =<< bvOne sym w
     case asBV e1B of
       Just bv -> bv @?= BV.mkBV w 3
       Nothing -> assertFailure $ unlines
@@ -1151,7 +1151,7 @@
     e2C <- bvAdd sym e2A e2B
     (_, e2C') <- annotateTerm sym $ unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e2C
     unsignedBVBounds e2C' @?= Just (2, 2)
-    e2D <- bvAdd sym e2C' =<< bvLit sym w (BV.one w)
+    e2D <- bvAdd sym e2C' =<< bvOne sym w
     case asBV e2D of
       Just bv -> bv @?= BV.mkBV w 3
       Nothing -> assertFailure $ unlines
diff --git a/test/InvariantSynthesis.hs b/test/InvariantSynthesis.hs
--- a/test/InvariantSynthesis.hs
+++ b/test/InvariantSynthesis.hs
@@ -75,8 +75,8 @@
   inv <- freshTotalUninterpFn sym (safeSymbol "inv") knownRepr knownRepr
   i <- freshConstant sym (safeSymbol "i") $ BaseBVRepr $ knownNat @64
   n <- freshConstant sym (safeSymbol "n") knownRepr
-  zero <- bvLit sym knownNat $ BV.zero knownNat
-  one <- bvLit sym knownNat $ BV.one knownNat
+  zero <- bvZero sym knownNat
+  one <- bvOne sym knownNat
   ult_1_n <- bvUlt sym one n
   inv_0_n <- applySymFn sym inv $ Empty :> zero :> n
   -- 1 < n ==> inv(0, n)
@@ -148,6 +148,7 @@
       failureZ3 = "failure with older Z3 versions; upgrade to at least 4.8.9"
   defaultMain $ testGroup "Tests" $
     [ synthesis_test "int" intProblem "cvc5" CVC5.runCVC5SyGuS CVC5.runCVC5InOverride
-    , skipPre4_8_9 failureZ3 $ synthesis_test "int" intProblem "z3" Z3.runZ3Horn Z3.runZ3InOverride
+    , skipPre4_8_9 failureZ3 $ synthesis_test "int" intProblem "z3" (\sym -> Z3.runZ3Horn sym False) Z3.runZ3InOverride
     , synthesis_test "bv" bvProblem "cvc5" CVC5.runCVC5SyGuS CVC5.runCVC5InOverride
+    , skipPre4_8_9 failureZ3 $ synthesis_test "bv->int" bvProblem  "z3" (\sym -> Z3.runZ3Horn sym True) Z3.runZ3InOverride
     ]
diff --git a/test/OnlineSolverTest.hs b/test/OnlineSolverTest.hs
--- a/test/OnlineSolverTest.hs
+++ b/test/OnlineSolverTest.hs
@@ -63,6 +63,8 @@
     ,  AnOnlineSolver @(SMT2.Writer CVC5) Proxy, cvc5Features, cvc5Options, Just cvc5Timeout)
   , (SolverName "Yices"
     , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)
+  , (SolverName "Bitwuzla"
+    , AnOnlineSolver @(SMT2.Writer Bitwuzla) Proxy, bitwuzlaFeatures, bitwuzlaOptions, Just bitwuzlaTimeout)
   , (SolverName "Boolector"
     , AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions, Just boolectorTimeout)
 #ifdef TEST_STP
@@ -378,6 +380,7 @@
                         , (SolverName "CVC4",       7.5  % Second)    -- CVC4 1.8
                         , (SolverName "CVC5",       0.40  % Second)   -- CVC5 1.0.0
                         , (SolverName "Yices",      2.9  % Second)    -- Yices 2.6.1
+                        , (SolverName "Bitwuzla",   0.51 % Second)    -- Bitwuzla 0.3.0
                         , (SolverName "Boolector",  7.2  % Second)    -- Boolector 3.2.1
                         , (SolverName "STP",        1.35 % Second)    -- STP 2.3.3
                         ]
diff --git a/test/ProbeSolvers.hs b/test/ProbeSolvers.hs
--- a/test/ProbeSolvers.hs
+++ b/test/ProbeSolvers.hs
@@ -27,7 +27,9 @@
       if r == ExitSuccess
       then let ol = lines o in
              return $ Right $ SolverVersion
-             $ if null ol then (solver <> " v??") else head ol
+             $ case ol of
+                 [] -> solver <> " v??"
+                 olh:_ -> olh
       else return $ Left $ solver <> " version error: " <> show r <> " /;/ " <> e
     Left (err :: SomeException) -> return $ Left $ solver <> " invocation error: " <> show err
 
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.5.1
+Version:       1.6
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com
 Copyright:     (c) Galois, Inc 2014-2023
@@ -16,7 +16,7 @@
   What4 is a generic library for representing values as symbolic formulae which may
   contain references to symbolic values, representing unknown variables.
   It provides support for communicating with a variety of SAT and SMT solvers,
-  including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal.
+  including Z3, CVC4, CVC5, Yices, Bitwuzla, Boolector, STP, and dReal.
 
   The data representation types make heavy use of GADT-style type indices
   to ensure type-correct manipulation of symbolic values.
@@ -126,7 +126,7 @@
     stm,
     temporary >= 1.2,
     template-haskell,
-    text >= 1.2.4.0 && < 2.1,
+    text >= 1.2.4.0 && < 2.2,
     th-lift >= 0.8.2 && < 0.9,
     th-lift-instances >= 0.1 && < 0.2,
     time >= 1.8 && < 1.13,
@@ -190,6 +190,7 @@
 
     What4.Solver
     What4.Solver.Adapter
+    What4.Solver.Bitwuzla
     What4.Solver.Boolector
     What4.Solver.CVC4
     What4.Solver.CVC5