diff --git a/crucible/src/Lang/Crucible/Backend/Online.hs b/crucible/src/Lang/Crucible/Backend/Online.hs
index 2cf05e4d9..6c81c62c8 100644
--- a/crucible/src/Lang/Crucible/Backend/Online.hs
+++ b/crucible/src/Lang/Crucible/Backend/Online.hs
@@ -64,6 +64,7 @@ module Lang.Crucible.Backend.Online
   ) where
 
 
+import           Control.Lens ( (^.) )
 import           Control.Monad
 import           Control.Monad.Fix (mfix)
 import           Control.Monad.Catch
@@ -172,12 +173,12 @@ newOnlineBackend ::
   ProblemFeatures ->
   IO (OnlineBackend solver scope st fs)
 newOnlineBackend sym feats =
-  do stk <- initAssumptionStack (B.exprCounter sym)
+  do stk <- initAssumptionStack (sym ^. B.exprCounter)
      procref <- newIORef SolverNotStarted
      featref <- newIORef feats
 
      mfix $ \bak ->
-       do extendConfig
+       do tryExtendConfig
             (backendOptions ++ onlineBackendOptions bak)
             (getConfiguration sym)
 
@@ -238,7 +239,7 @@ withYicesOnlineBackend ::
 withYicesOnlineBackend sym unsatFeat extraFeatures action =
   let feat = Yices.yicesDefaultFeatures .|. unsatFeaturesToProblemFeatures unsatFeat  .|. extraFeatures in
   withOnlineBackend sym feat $ \bak ->
-    do liftIO $ extendConfig Yices.yicesOptions (getConfiguration sym)
+    do liftIO $ tryExtendConfig Yices.yicesOptions (getConfiguration sym)
        action bak
 
 type Z3OnlineBackend scope st fs = OnlineBackend (SMT2.Writer Z3.Z3) scope st fs
@@ -264,7 +265,7 @@ withZ3OnlineBackend ::
 withZ3OnlineBackend sym unsatFeat extraFeatures action =
   let feat = (SMT2.defaultFeatures Z3.Z3 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in
   withOnlineBackend sym feat $ \bak ->
-    do liftIO $ extendConfig Z3.z3Options (getConfiguration sym)
+    do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym)
        action bak
 
 type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs
@@ -285,7 +286,7 @@ withBoolectorOnlineBackend ::
 withBoolectorOnlineBackend sym unsatFeat action =
   let feat = (SMT2.defaultFeatures Boolector.Boolector .|. unsatFeaturesToProblemFeatures unsatFeat) in
   withOnlineBackend sym feat $ \bak -> do
-    liftIO $ extendConfig Boolector.boolectorOptions (getConfiguration sym)
+    liftIO $ tryExtendConfig Boolector.boolectorOptions (getConfiguration sym)
     action bak
 
 type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs
@@ -311,7 +312,7 @@ withCVC4OnlineBackend ::
 withCVC4OnlineBackend sym unsatFeat extraFeatures action =
   let feat = (SMT2.defaultFeatures CVC4.CVC4 .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in
   withOnlineBackend sym feat $ \bak -> do
-    liftIO $ extendConfig CVC4.cvc4Options (getConfiguration sym)
+    liftIO $ tryExtendConfig CVC4.cvc4Options (getConfiguration sym)
     action bak
 
 type STPOnlineBackend scope st fs = OnlineBackend (SMT2.Writer STP.STP) scope st fs
@@ -334,7 +335,7 @@ withSTPOnlineBackend ::
   m a
 withSTPOnlineBackend sym action =
   withOnlineBackend sym (SMT2.defaultFeatures STP.STP) $ \bak -> do
-    liftIO $ extendConfig STP.stpOptions (getConfiguration sym)
+    liftIO $ tryExtendConfig STP.stpOptions (getConfiguration sym)
     action bak
 
 -- | Shutdown any currently-active solver process.
diff --git a/crucible/src/Lang/Crucible/Backend/Simple.hs b/crucible/src/Lang/Crucible/Backend/Simple.hs
index a56cc9b32..c19f5b4ed 100644
--- a/crucible/src/Lang/Crucible/Backend/Simple.hs
+++ b/crucible/src/Lang/Crucible/Backend/Simple.hs
@@ -29,6 +29,7 @@ module Lang.Crucible.Backend.Simple
   , B.Flags
   ) where
 
+import           Control.Lens ( (^.) )
 import           Control.Monad (void)
 
 import           What4.Config
@@ -59,8 +60,8 @@ newSimpleBackend ::
   B.ExprBuilder t st fs ->
   IO (SimpleBackend t st fs)
 newSimpleBackend sym =
-  do as <- AS.initAssumptionStack (B.exprCounter sym)
-     extendConfig backendOptions (getConfiguration sym)
+  do as <- AS.initAssumptionStack (sym ^. B.exprCounter)
+     tryExtendConfig backendOptions (getConfiguration sym)
      return SimpleBackend
             { sbAssumptionStack = as
             , sbExprBuilder = sym
diff --git a/crucible/src/Lang/Crucible/Simulator/PathSatisfiability.hs b/crucible/src/Lang/Crucible/Simulator/PathSatisfiability.hs
index ae6455b22..a55c31303 100644
--- a/crucible/src/Lang/Crucible/Simulator/PathSatisfiability.hs
+++ b/crucible/src/Lang/Crucible/Simulator/PathSatisfiability.hs
@@ -64,7 +64,7 @@ pathSatisfiabilityFeature :: forall sym.
         we can determine about the given predicate. -} ->
   IO (GenericExecutionFeature sym)
 pathSatisfiabilityFeature sym considerSatisfiability =
-  do extendConfig pathSatOptions (getConfiguration sym)
+  do tryExtendConfig pathSatOptions (getConfiguration sym)
      pathSatOpt <- liftIO $ getOptionSetting checkPathSatisfiability (getConfiguration sym)
      return $ GenericExecutionFeature $ onStep pathSatOpt
 
diff --git a/dependencies/what4 b/dependencies/what4
index 042a8112b..f42f64b51 160000
--- a/dependencies/what4
+++ b/dependencies/what4
@@ -1 +1 @@
-Subproject commit 042a8112b1d2b97b91e3399bb976eebe33fc60b8
+Subproject commit f42f64b51e735a26460bb87b7d34de2188275afb