diff --git a/deps/crucible b/deps/crucible
index 1d2d95d2..994b4f94 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 1d2d95d232eb2aae076d68021e1d75d322968595
+Subproject commit 994b4f944630c561b9390f2a5f8d53d40f7318e5
diff --git a/deps/semmc b/deps/semmc
index a3b8b89b..fd356864 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit a3b8b89b9e88c94aab2ec6e06f993edcc9126cea
+Subproject commit fd3568642e1ffc0c31dab172f4f430c3c009286c
diff --git a/symbolic/ChangeLog.md b/symbolic/ChangeLog.md
index ecde0643..6c87f215 100644
--- a/symbolic/ChangeLog.md
+++ b/symbolic/ChangeLog.md
@@ -34,4 +34,6 @@
    - `addExtraBlock`
    - `freshValueIndex`
 
-- `Data.Macaw.Symbolic.Memory.newGlobalMemory` now has a `?memOpts :: MemOptions` constraint.
+- The following functions now have a `?memOpts :: MemOptions` constraint:
+  - `Data.Macaw.Symbolic.Memory.newGlobalMemory`
+  - `Data.Macaw.Symbolic.MemOps.{doWriteMem,doCondWriteMem}`
diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
index fba78e7d..4aa6c392 100644
--- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
@@ -1073,7 +1073,7 @@ doCondReadMem bak mem ptrWidth memRep cond ptr def = hasPtrClass ptrWidth $
 --     arg5 : Address to write to
 --     arg6 : Value to write
 doWriteMem ::
-  (IsSymBackend sym bak, Mem.HasLLVMAnn sym) =>
+  (IsSymBackend sym bak, Mem.HasLLVMAnn sym, ?memOpts :: Mem.MemOptions) =>
   bak ->
   MemImpl sym ->
   M.AddrWidthRepr ptrW ->
@@ -1104,7 +1104,7 @@ doWriteMem bak mem ptrWidth memRep ptr val = hasPtrClass ptrWidth $
 --     arg6 : Address to write to
 --     arg7 : Value to write
 doCondWriteMem ::
-  (IsSymBackend sym bak, Mem.HasLLVMAnn sym) =>
+  (IsSymBackend sym bak, Mem.HasLLVMAnn sym, ?memOpts :: Mem.MemOptions) =>
   bak ->
   MemImpl sym ->
   M.AddrWidthRepr ptrW ->