diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index fdb853f076..53b461ed5b 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -1131,7 +1131,7 @@ verifyPoststate opts sc cc mspec env0 globals ret =
        io $
        runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $
        do matchResult
-          learnCond opts sc cc mspec PostState (mspec ^. MS.csPostState)
+          learnCond opts sc cc mspec PostState (mspec ^. MS.csGlobalAllocs) (mspec ^. MS.csPostState)
 
      st <-
        case matchPost of
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 0aa18e01ef..806777ac14 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -592,7 +592,7 @@ methodSpecHandler_prestate opts sc cc args cs =
 
        sequence_ [ matchArg opts sc cc cs PreState x y z | (x, y, z) <- xs]
 
-       learnCond opts sc cc cs PreState (cs ^. MS.csPreState)
+       learnCond opts sc cc cs PreState (cs ^. MS.csGlobalAllocs) (cs ^. MS.csPreState)
 
 
 -- | Use a method spec to override the behavior of a function.
@@ -619,14 +619,15 @@ learnCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWi
           -> LLVMCrucibleContext arch
           -> MS.CrucibleMethodSpecIR (LLVM arch)
           -> PrePost
+          -> [MS.AllocGlobal (LLVM arch)]
           -> MS.StateSpec (LLVM arch)
           -> OverrideMatcher (LLVM arch) md ()
-learnCond opts sc cc cs prepost ss =
+learnCond opts sc cc cs prepost globals ss =
   do let loc = cs ^. MS.csLoc
      matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos)
      traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions)
      enforcePointerValidity cc loc ss
-     enforceDisjointness loc ss
+     enforceDisjointness cc loc globals ss
      enforceCompleteSubstitution loc ss
 
 
@@ -743,12 +744,15 @@ enforcePointerValidity cc loc ss =
 -- allowed to alias other read-only allocations, however.
 enforceDisjointness ::
   (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  LLVMCrucibleContext arch ->
   W4.ProgramLoc ->
+  [MS.AllocGlobal (LLVM arch)] ->
   MS.StateSpec (LLVM arch) ->
   OverrideMatcher (LLVM arch) md ()
-enforceDisjointness loc ss =
+enforceDisjointness cc loc globals ss =
   do sym <- Ov.getSymInterface
      sub <- OM (use setupValueSub)
+     mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc
      let (allocsRW, allocsRO) = Map.partition (view isMut) (view MS.csAllocs ss)
          memsRW = Map.elems $ Map.intersectionWith (,) allocsRW sub
          memsRO = Map.elems $ Map.intersectionWith (,) allocsRO sub
@@ -761,6 +765,19 @@ enforceDisjointness loc ss =
         , q <- ps ++ memsRO
         ]
 
+     -- Ensure that all RW and RO regions are disjoint from mutable
+     -- global regions.
+     let resolveAllocGlobal g@(LLVMAllocGlobal _ nm) =
+           do ptr <- liftIO $ Crucible.doResolveGlobal sym mem nm
+              pure (g, ptr)
+     globals' <- traverse resolveAllocGlobal globals
+     sequence_
+       [ enforceDisjointAllocGlobal sym loc p q
+       | p <- memsRW ++ memsRO
+       , q <- globals'
+       ]
+
+-- | Assert that two LLVM allocations are disjoint from each other.
 enforceDisjointAllocSpec ::
   (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
   Sym -> W4.ProgramLoc ->
@@ -788,6 +805,26 @@ enforceDisjointAllocSpec sym loc
      addAssert c $ Crucible.SimError loc $
        Crucible.AssertFailureSimError msg ""
 
+-- | Assert that an LLVM allocation is disjoint from a global region.
+enforceDisjointAllocGlobal ::
+  Sym -> W4.ProgramLoc ->
+  (LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) ->
+  (LLVMAllocGlobal arch, LLVMPtr (Crucible.ArchWidth arch)) ->
+  OverrideMatcher (LLVM arch) md ()
+enforceDisjointAllocGlobal sym loc
+  (LLVMAllocSpec _pmut _pty _palign psz _ploc, p)
+  (LLVMAllocGlobal _qloc (L.Symbol qname), q) =
+  do let Crucible.LLVMPointer pblk _ = p
+     let Crucible.LLVMPointer qblk _ = q
+     c <- liftIO $ W4.notPred sym =<< W4.natEq sym pblk qblk
+     let msg =
+           "Memory regions not disjoint: "
+           ++ "(base=" ++ show (Crucible.ppPtr p) ++ ", size=" ++ show psz ++ ")"
+           ++ " and "
+           ++ "global " ++ show qname ++ " (base=" ++ show (Crucible.ppPtr q) ++ ")"
+     addAssert c $ Crucible.SimError loc $
+       Crucible.AssertFailureSimError msg ""
+
 ------------------------------------------------------------------------
 
 -- | For each points-to statement read the memory value through the