diff --git a/deps/crucible b/deps/crucible
index 97be912e7a..b2f49a5fa5 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 97be912e7a08699e90f19aba861872022e4ff46d
+Subproject commit b2f49a5fa56501aecf13f1ef4f8242923910131a
diff --git a/intTests/test_jvm_unsound/test.saw b/intTests/test_jvm_unsound/test.saw
index a8588a3830..21a598202b 100644
--- a/intTests/test_jvm_unsound/test.saw
+++ b/intTests/test_jvm_unsound/test.saw
@@ -83,8 +83,7 @@ jvm_verify c "test_b" [set_ov_2] false
   z3;
 
 // It should be impossible to verify the bogus set_spec_1.
-// FIXME: this should fail
-jvm_verify c "set" [] false set_spec_1 z3;
+fails (jvm_verify c "set" [] false set_spec_1 z3);
 
 // It should be impossible to verify the bogus set_spec_2.
 // FIXME: this should fail
diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index ea18f8ac71..547aed569b 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -321,6 +321,7 @@ verifyPrestate ::
       Crucible.SymGlobalState Sym)
 verifyPrestate cc mspec globals0 =
   do let sym = cc^.jccBackend
+     let jc = cc^.jccJVMContext
      let preallocs = mspec ^. MS.csPreState . MS.csAllocs
      let tyenv = MS.csAllocations mspec
      let nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
@@ -330,9 +331,15 @@ verifyPrestate cc mspec globals0 =
 
      --let cvar = CJ.dynamicClassTable (cc^.jccJVMContext)
      --let Just mem = Crucible.lookupGlobal lvar globals
+     let postPointsTos = mspec ^. MS.csPostState . MS.csPointsTos
+
+     -- make static fields mentioned in post-state section writable
+     let updatedStaticFields = [ fid | JVMPointsToStatic _ fid _ <- postPointsTos ]
+     let makeWritable gs fid = CJ.doStaticFieldWritable sym jc gs fid (W4.truePred sym)
+     globals0' <- liftIO $ foldM makeWritable globals0 updatedStaticFields
 
      -- Allocate objects in memory for each 'jvm_alloc'
-     (env, globals1) <- runStateT (traverse (doAlloc cc . snd) preallocs) globals0
+     (env, globals1) <- runStateT (traverse (doAlloc cc . snd) preallocs) globals0'
 
      globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1
      cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions)
@@ -746,7 +753,10 @@ setupGlobalState sym jc =
   do classTab <- setupDynamicClassTable sym jc
      let classTabVar = CJ.dynamicClassTable jc
      let globals0 = Crucible.insertGlobal classTabVar classTab Crucible.emptyGlobals
-     let declareGlobal var = Crucible.insertGlobal var CJ.unassignedJVMValue
+     let writable = W4.falsePred sym -- static fields default to read-only
+     let declareGlobal info =
+           Crucible.insertGlobal (CJ.staticFieldWritable info) writable .
+           Crucible.insertGlobal (CJ.staticFieldValue info) CJ.unassignedJVMValue
      return $ foldr declareGlobal globals0 (Map.elems (CJ.staticFields jc))
 
 setupDynamicClassTable :: Sym -> CJ.JVMContext -> IO (Crucible.RegValue Sym CJ.JVMClassTableType)