diff --git a/patches/what4-1.3.patch b/patches/what4-1.3.patch
index 521cda5cabcfd86b06cec552b2c39a422d818cfd..8dbb1193f2ccfc0ad93cb52d09f7dae2629dd761 100644
--- a/patches/what4-1.3.patch
+++ b/patches/what4-1.3.patch
@@ -28,6 +28,34 @@ index 6d91cda..8f247c3 100644
  
  -- | Record variables in a predicate that we are checking satisfiability of.
  recordAssertionVars :: Scope
+diff --git a/src/What4/Interface.hs b/src/What4/Interface.hs
+index edec041..c9af5ef 100644
+--- a/src/What4/Interface.hs
++++ b/src/What4/Interface.hs
+@@ -2589,8 +2589,9 @@ bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym)
+              -> NatRepr w
+              -> Vector.Vector n (SymBV sym w)
+              -> IO (SymBV sym (n * w))
+-bvJoinVector sym w =
+-  coerce $ Vector.joinWithM @IO @(SymBV' sym) @n bvConcat' w
++bvJoinVector sym w v = do
++  bv <- Vector.joinWithM @IO @(SymBV' sym) @n bvConcat' w $ coerce v
++  pure $ coerce bv
+   where bvConcat' :: forall l. (1 <= l)
+                   => NatRepr l
+                   -> SymBV' sym w
+@@ -2607,8 +2608,9 @@ bvSplitVector :: forall sym n w. (IsExprBuilder sym, 1 <= w, 1 <= n)
+               -> NatRepr w
+               -> SymBV sym (n * w)
+               -> IO (Vector.Vector n (SymBV sym w))
+-bvSplitVector sym n w x =
+-  coerce $ Vector.splitWithA @IO BigEndian bvSelect' n w (MkSymBV' @sym x)
++bvSplitVector sym n w x = do
++  bv <- Vector.splitWithA @IO BigEndian bvSelect' n w (MkSymBV' @sym x)
++  pure $ coerce bv
+   where
+     bvSelect' :: forall i. (i + w <= n * w)
+               => NatRepr (n * w)
 diff --git a/src/What4/Utils/AbstractDomains.hs b/src/What4/Utils/AbstractDomains.hs
 index 8b89aa5..77c8399 100644
 --- a/src/What4/Utils/AbstractDomains.hs