diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
index c9b96aa04..7af6b67a3 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
@@ -1042,12 +1042,7 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs
           gimap = view Crucible.globalInitMap mtrans
       case Map.lookup symbol gimap of
         Just (g, Right (mt, _)) -> ccWithBackend cc $ \bak ->
-          do when (L.gaConstant $ L.globalAttrs g) . throwMethodSpec mspec $ mconcat
-               [ "Global variable \""
-               , name
-               , "\" is not mutable"
-               ]
-             let sz = Crucible.memTypeSize (Crucible.llvmDataLayout ?lc) mt
+          do let sz = Crucible.memTypeSize (Crucible.llvmDataLayout ?lc) mt
              sz' <- W4.bvLit sym ?ptrWidth $ Crucible.bytesToBV ?ptrWidth sz
              alignment <-
                case L.globalAlign g of
@@ -1061,7 +1056,10 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs
                        ]
                      Just al -> return al
                  _ -> pure $ Crucible.memTypeAlign (Crucible.llvmDataLayout ?lc) mt
-             (ptr, mem') <- Crucible.doMalloc bak Crucible.GlobalAlloc Crucible.Mutable name mem sz' alignment
+             let mutability
+                   | L.gaConstant (L.globalAttrs g) = Crucible.Immutable
+                   | otherwise = Crucible.Mutable
+             (ptr, mem') <- Crucible.doMalloc bak Crucible.GlobalAlloc mutability name mem sz' alignment
              pure $ Crucible.registerGlobal mem' [symbol] ptr
         _ -> throwMethodSpec mspec $ mconcat
           [ "Global variable \""
@@ -1701,6 +1699,7 @@ setupLLVMCrucibleContext pathSat lm action =
      what4PushMuxOps <- gets rwWhat4PushMuxOps
      laxPointerOrdering <- gets rwLaxPointerOrdering
      laxLoadsAndStores <- gets rwLaxLoadsAndStores
+     globalAllocMode <- gets rwLLVMGlobalAllocMode
      noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant
      pathSatSolver <- gets rwPathSatSolver
      what4Eval <- gets rwWhat4Eval
@@ -1759,8 +1758,17 @@ setupLLVMCrucibleContext pathSat lm action =
                                  intrinsics halloc stdout
                                  bindings (Crucible.llvmExtensionImpl ?memOpts)
                                  Common.SAWCruciblePersonality
-               mem <- Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans)
-                        =<< Crucible.initializeMemoryConstGlobals bak ctx llvm_mod
+               
+               mem <-
+                case globalAllocMode of
+                  LLVMAllocConstantGlobals ->
+                    Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans)
+                    =<< Crucible.initializeMemoryConstGlobals bak ctx llvm_mod
+                  LLVMAllocAllGlobals ->
+                    Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans)
+                    =<< Crucible.initializeAllMemory bak ctx llvm_mod
+                  LLVMAllocNoGlobals ->
+                    Crucible.initializeMemory (const False) bak ctx llvm_mod
 
                let globals  = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem
 
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs b/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs
index 360bbeb96..134ee3915 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs
@@ -67,6 +67,8 @@ module SAWCentral.Crucible.LLVM.CrucibleLLVM
     -- * Re-exports from "Lang.Crucible.LLVM.Globals"
   , GlobalInitializerMap
   , initializeMemoryConstGlobals
+  , initializeAllMemory
+  , initializeMemory
   , makeGlobalMap
   , populateConstGlobals
     -- * Re-exports from "Lang.Crucible.LLVM.Translation"
@@ -164,7 +166,9 @@ import Lang.Crucible.LLVM.TypeContext
 import qualified Lang.Crucible.LLVM.TypeContext as TyCtx
 
 import Lang.Crucible.LLVM.Globals
-  (GlobalInitializerMap, initializeMemoryConstGlobals, makeGlobalMap, populateConstGlobals)
+  (GlobalInitializerMap, makeGlobalMap, populateConstGlobals,
+   initializeAllMemory, initializeMemoryConstGlobals,
+   initializeMemory)
 
 import Lang.Crucible.LLVM.Translation
   (llvmMemVar, transContext, llvmPtrWidth, llvmTypeCtx,
diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs
index 2beb60f9e..17ba012e4 100644
--- a/saw-central/src/SAWCentral/Value.hs
+++ b/saw-central/src/SAWCentral/Value.hs
@@ -70,6 +70,8 @@ module SAWCentral.Value (
     TopLevelRW(..),
     -- used by ... a lot of places, let's not try to make a list just yet
     TopLevel(..),
+    -- Used by TopLevelRW
+    LLVMGlobalAllocMode(..),
     -- used by SAWCentral.Builtins, SAWScript.REPL.Monad, SAWScript.Interpreter,
     --    SAWServer.TopLevel
     runTopLevel,
@@ -809,6 +811,12 @@ data JavaCodebase =
     -- ^ At least one Java-related command has been invoked successfully.
     -- We cache the resulting 'JSS.Codebase' for subsequent commands.
 
+data LLVMGlobalAllocMode
+  = LLVMAllocConstantGlobals -- ^ constants are allocated, globals need llvm_alloc_global
+  | LLVMAllocAllGlobals   -- ^ all globals are allocated
+  | LLVMAllocNoGlobals -- ^ No globals are allocated, use llvm_alloc_global and llvm_alloc_constant
+  deriving (Show)
+
 data TopLevelRW =
   TopLevelRW
   { rwValueInfo  :: Map SS.LName (SS.PrimitiveLifecycle, SS.Schema, Value)
@@ -847,6 +855,7 @@ data TopLevelRW =
   , rwLaxLoadsAndStores :: Bool
   , rwLaxPointerOrdering :: Bool
   , rwDebugIntrinsics :: Bool
+  , rwLLVMGlobalAllocMode :: LLVMGlobalAllocMode
 
   -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing"
   , rwWhat4HashConsing :: Bool
diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs
index 1c45518d9..8fa3186e6 100644
--- a/saw-script/src/SAWScript/Interpreter.hs
+++ b/saw-script/src/SAWScript/Interpreter.hs
@@ -1079,6 +1079,7 @@ buildTopLevelEnv proxy opts scriptArgv =
                    , rwLaxArith = False
                    , rwLaxPointerOrdering = False
                    , rwLaxLoadsAndStores = False
+                   , rwLLVMGlobalAllocMode = LLVMAllocConstantGlobals
                    , rwDebugIntrinsics = True
                    , rwWhat4HashConsing = False
                    , rwWhat4HashConsingX86 = False
@@ -1885,6 +1886,11 @@ disable_lax_loads_and_stores = do
   rw <- getTopLevelRW
   putTopLevelRW rw { rwLaxLoadsAndStores = False }
 
+llvm_set_global_alloc_mode :: LLVMGlobalAllocMode -> TopLevel ()
+llvm_set_global_alloc_mode mode = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwLLVMGlobalAllocMode = mode }
+
 set_solver_cache_path :: Text -> TopLevel ()
 set_solver_cache_path pathtxt = do
   let path :: FilePath = Text.unpack pathtxt
@@ -5341,6 +5347,22 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_null`." ]
 
+  , prim "llvm_alloc_all_globals" "TopLevel ()"
+    (pureVal (llvm_set_global_alloc_mode LLVMAllocAllGlobals))
+    Experimental
+    [ "Enable allocation of all constant and mutable globals automatically."
+    ]
+
+  , prim "llvm_alloc_constant_globals" "TopLevel ()"
+    (pureVal (llvm_set_global_alloc_mode LLVMAllocConstantGlobals))
+    Experimental
+    [ "Enable allocation of constant globals automatically. (default)" ]
+  
+  , prim "llvm_alloc_no_globals" "TopLevel ()"
+    (pureVal (llvm_set_global_alloc_mode LLVMAllocNoGlobals))
+    Experimental
+    [ "Disable allocation of all globals automatically." ]
+
   , prim "llvm_global"
     "String -> SetupValue"
     (pureVal CIR.anySetupGlobal)