diff --git a/.github/scripts/install-libsecp256k1.sh b/.github/scripts/install-libsecp256k1.sh
index 8f0f9940b..b19207433 100755
--- a/.github/scripts/install-libsecp256k1.sh
+++ b/.github/scripts/install-libsecp256k1.sh
@@ -3,7 +3,7 @@ set -eux -o pipefail
 
 ## The following script builds and installs libsecp256k1 to ~/.local/lib
 
-INSTALL_VERSION=0.5.0
+INSTALL_VERSION=0.5.1
 
 if [[ "$(uname -s)" =~ ^MSYS_NT.* ]]; then
     echo "This script is only meant to run on Windows under MSYS2"
diff --git a/.github/workflows/bitwuzla-windows.yml b/.github/workflows/bitwuzla-windows.yml
index 37b5d2b94..fe003e60c 100644
--- a/.github/workflows/bitwuzla-windows.yml
+++ b/.github/workflows/bitwuzla-windows.yml
@@ -2,7 +2,7 @@ on:
   workflow_call:
 
 env:
-    BITWUZLA_VERSION: 0.5.0
+    BITWUZLA_VERSION: 0.6.1
 
 jobs:
   build:
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index e143b39cc..5d7e5cace 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -109,7 +109,7 @@ jobs:
             openssl:p
             z3:p
             go:p
-      - uses: haskell-actions/setup@v2.7.0
+      - uses: haskell-actions/setup@v2.7.7
         id: setup
         with:
           ghc-version: '9.6.5'
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 627e3f1bb..951d87644 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - When a staticcall is made to a contract that does not exist, we overapproxiate
   and return symbolic values
 
+## Fixed
+- We now try to simplify expressions fully before trying to cast them to a concrete value
+  This should improve issues when "Unexpected Symbolic Arguments to Opcode" was
+  unnecessarily output
+
+
 ## [0.54.2] - 2024-12-12
 
 ## Fixed
diff --git a/cli/cli.hs b/cli/cli.hs
index 516158115..369b65e61 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -46,6 +46,7 @@ import EVM.Types hiding (word, Env, Symbolic)
 import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
+import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
 
 data AssertionType = DSTest | Forge
   deriving (Eq, Show, Read, ParseField)
@@ -489,7 +490,7 @@ vmFromCommand cmd = do
       putStrLn "Error, must provide at least (rpc + address) or code"
       exitFailure
 
-  let ts' = case maybeLitWord ts of
+  let ts' = case maybeLitWordSimp ts of
         Just t -> t
         Nothing -> internalError "unexpected symbolic timestamp when executing vm test"
 
@@ -511,7 +512,7 @@ vmFromCommand cmd = do
                     then InitCode bs mempty
                     else RuntimeCode (ConcreteRuntimeCode bs)
         address = if cmd.create
-                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddr origin) (W64 $ word64 (.nonce) 0))
+                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0))
                   else addr (.address) (LitAddr 0xacab)
 
         vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts
diff --git a/doc/src/exec.md b/doc/src/exec.md
index f85d27145..01b9bf0f2 100644
--- a/doc/src/exec.md
+++ b/doc/src/exec.md
@@ -1,6 +1,6 @@
 # `hevm exec`
 
-Run an EVM computation using specified parameters, using an interactive debugger when `--debug` flag is given.
+Run an EVM computation using specified parameters.
 
 ```
 Usage: hevm exec [--code TEXT] [--calldata TEXT] [--address ADDR]
@@ -38,7 +38,8 @@ Available options:
   --rpc TEXT               Fetch state from a remote node
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE Foundry or CombinedJSON project
+  --project-type PROJ      Foundry or CombinedJSON project (default: Foundry)
+  --assertion-type ASSERT  Assertions as per Forge or DSTest (default: Forge)
 ```
 
 Minimum required flags: either you must provide `--code` or you must both pass
diff --git a/flake.lock b/flake.lock
index e32b815af..04c1e6bc6 100644
--- a/flake.lock
+++ b/flake.lock
@@ -120,11 +120,11 @@
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1725194671,
-        "narHash": "sha256-tLGCFEFTB5TaOKkpfw3iYT9dnk4awTP/q4w+ROpMfuw=",
+        "lastModified": 1733229606,
+        "narHash": "sha256-FLYY5M0rpa5C2QAE3CKLYAM6TwbKicdRK6qNrSHlNrE=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "b833ff01a0d694b910daca6e2ff4a3f26dee478c",
+        "rev": "566e53c2ad750c84f6d31f9ccb9d00f823165550",
         "type": "github"
       },
       "original": {
diff --git a/hevm.cabal b/hevm.cabal
index d57240cf6..2430b8349 100644
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -146,11 +146,11 @@ library
     containers                        >= 0.6.0 && < 0.7,
     transformers                      >= 0.5 && < 0.7,
     tree-view                         >= 0.5 && < 0.6,
-    aeson                             >= 2.0.0 && < 2.2,
-    bytestring                        >= 0.11.3.1 && < 0.12,
+    aeson                             >= 2.0.0 && < 2.3,
+    bytestring                        >= 0.11.3.1 && < 0.13,
     scientific                        >= 0.3.6 && < 0.4,
     binary                            >= 0.8.6 && < 0.9,
-    text                              >= 1.2.3 && < 2.1,
+    text                              >= 1.2.3 && < 2.2,
     unordered-containers              >= 0.2.10 && < 0.3,
     vector                            >= 0.12.1 && < 0.14,
     base16                            >= 1.0 && < 1.1,
@@ -231,12 +231,10 @@ common test-base
     base,
     containers,
     directory,
-    extra,
     bytestring,
     filemanip,
     filepath,
     hevm,
-    here,
     mtl,
     process,
     tasty,
@@ -284,6 +282,8 @@ test-suite test
     base16,
     binary,
     data-dword,
+    extra,
+    here,
     time,
     regex
 
diff --git a/src/EVM.hs b/src/EVM.hs
index 6d319c71b..08749415a 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -24,6 +24,7 @@ import EVM.Types qualified as Expr (Expr(Gas))
 import EVM.Sign qualified
 import EVM.Concrete qualified as Concrete
 import EVM.CheatsTH
+import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp)
 
 import Control.Monad (unless, when)
 import Control.Monad.ST (ST)
@@ -282,7 +283,7 @@ getOpW8 state = case state.code of
       RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs state.pc
       RuntimeCode (SymbolicRuntimeCode ops) ->
         fromMaybe (internalError "could not analyze symbolic code") $
-          maybeLitByte $ ops V.! state.pc
+          maybeLitByteSimp $ ops V.! state.pc
 
 getOpName :: forall (t :: VMType) s . FrameState t s -> [Char]
 getOpName state = intToOpName $ fromEnum $ getOpW8 state
@@ -305,12 +306,9 @@ exec1 = do
     stk  = vm.state.stack
     self = vm.state.contract
     this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)
-
     fees@FeeSchedule {..} = vm.block.schedule
-
     doStop = finishFrame (FrameReturned mempty)
-
-    litSelf = maybeLitAddr self
+    litSelf = maybeLitAddrSimp self
 
   if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0xa then do
     -- call to precompile
@@ -750,7 +748,7 @@ exec1 = do
                         Lit v -> v
                         _ -> 0
                     storage_cost =
-                      case (maybeLitWord current, maybeLitWord new) of
+                      case (maybeLitWordSimp current, maybeLitWordSimp new) of
                         (Just current', Just new') ->
                            if (current' == new') then g_sload
                            else if (current' == original) && (original == 0) then g_sset
@@ -768,7 +766,7 @@ exec1 = do
                     assign (#state % #stack) xs
                     modifying (#env % #contracts % ix self % #storage) (writeStorage x new)
 
-                    case (maybeLitWord current, maybeLitWord new) of
+                    case (maybeLitWordSimp current, maybeLitWordSimp new) of
                        (Just current', Just new') ->
                           unless (current' == new') $
                             if current' == original then
@@ -923,7 +921,7 @@ exec1 = do
                 output <- readMemory xOffset xSize
                 let
                   codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")
-                               . maybeLitWord . bufLength $ output
+                               . maybeLitWordSimp . bufLength $ output
                   maxsize = vm.block.maxCodeSize
                   creation = case vm.frames of
                     [] -> vm.tx.isCreate
@@ -961,6 +959,8 @@ exec1 = do
                   case gasTryFrom xGas of
                     Left _ -> vmError IllegalOverflow
                     Right gas ->
+                      -- NOTE: we don't update overrideCaller in this case because
+                      -- forge-std doesn't. see: https://github.com/foundry-rs/foundry/pull/8863
                       delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
                         \_ -> touchAccount self
             _ -> underrun
@@ -1195,7 +1195,7 @@ precompiledContract this xGas precompileAddr recipient xValue inOffset inSize ou
       vm <- get
       case result' of
         Nothing -> case stk of
-          x:_ -> case maybeLitWord x of
+          x:_ -> case maybeLitWordSimp x of
             Just 0 ->
               pure ()
             Just 1 ->
@@ -1610,28 +1610,28 @@ forceAddr n msg continue = case wordToAddr n of
   Just c -> continue c
 
 forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
-forceConcrete n msg continue = case maybeLitWord n of
+forceConcrete n msg continue = case maybeLitWordSimp n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
   Just c -> continue c
 
 forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
-forceConcreteAddr n msg continue = case maybeLitAddr n of
+forceConcreteAddr n msg continue = case maybeLitAddrSimp n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
   Just c -> continue c
 
 forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
-forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of
+forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddrSimp n, maybeLitAddrSimp m) of
   (Just c, Just d) -> continue (c,d)
   _ -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n, m])
 
 forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
-forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of
+forceConcrete2 (n,m) msg continue = case (maybeLitWordSimp n, maybeLitWordSimp m) of
   (Just c, Just d) -> continue (c, d)
   _ -> do
     vm <- get
@@ -1683,7 +1683,7 @@ accessAccountForGas addr = do
 accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool
 accessStorageForGas addr key = do
   accessedStrkeys <- use (#tx % #subState % #accessedStorageKeys)
-  case maybeLitWord key of
+  case maybeLitWordSimp key of
     Just litword -> do
       let accessed = member (addr, litword) accessedStrkeys
       assign (#tx % #subState % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)
@@ -1708,7 +1708,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
   input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))
   calldata <- readMemory inOffset inSize
   abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)
-  let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWord abi) calldata vm.env.contracts vm.tx.subState
+  let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWordSimp abi) calldata vm.env.contracts vm.tx.subState
 
   pushTrace $ FrameTrace newContext
   next
@@ -1717,7 +1717,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
                     { state = vm1.state { stack = xs }
                     , context = newContext
                     }
-  case maybeLitWord abi of
+  case maybeLitWordSimp abi of
     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just (unsafeInto -> abi') ->
       case Map.lookup abi' cheatActions of
@@ -2073,7 +2073,7 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
               _ -> do
                 burn' xGas $ do
                   calldata <- readMemory xInOffset xInSize
-                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
+                  abi <- maybeLitWordSimp . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
                   let newContext = CallContext
                                     { target    = xTo
                                     , context   = xContext
@@ -2670,7 +2670,7 @@ isValidJumpDest vm x = let
       UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code"
       InitCode ops _ -> BS.indexMaybe ops x
       RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x
-      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte
+      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByteSimp
   in case op of
        Nothing -> False
        Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))
@@ -2709,7 +2709,7 @@ mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
       let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops)
       in m >> pure v
       where
-        go v (0, !i, !j, !m) x = case maybeLitByte x of
+        go v (0, !i, !j, !m) x = case maybeLitByteSimp x of
           Just x' -> if x' >= 0x60 && x' <= 0x7f
             -- start of PUSH op --
                      then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)
@@ -2734,7 +2734,7 @@ vmOp vm =
         RuntimeCode (ConcreteRuntimeCode xs') ->
           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')
         RuntimeCode (SymbolicRuntimeCode xs') ->
-          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')
+          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByteSimp $ xs' V.! i , V.toList $ V.drop i xs')
   in if (opslen code' < i)
      then Nothing
      else Just (readOp op pushdata)
@@ -2762,7 +2762,7 @@ mkCodeOps contractCode =
         Nothing ->
           mempty
         Just (x, xs') ->
-          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x
+          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByteSimp x
               j = opSize x'
           in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)
 
diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
index 58d97dcc2..861c40e8f 100644
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -60,6 +60,7 @@ module EVM.ABI
 
 import EVM.Expr (readWord, isLitWord)
 import EVM.Types
+import EVM.Expr (maybeLitWordSimp)
 
 import Control.Applicative ((<|>))
 import Control.Monad (replicateM, replicateM_, forM_, void)
@@ -511,7 +512,7 @@ decodeBuf tps buf =
   else
     let
       vs = decodeStaticArgs 0 (length tps) buf
-      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
+      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWordSimp vs)
     in if not (all isLitWord vs)
        then SAbi vs
        else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs
index c6e1e4e9f..c415cf0b3 100644
--- a/src/EVM/Dapp.hs
+++ b/src/EVM/Dapp.hs
@@ -4,6 +4,7 @@ import EVM.ABI
 import EVM.Concrete
 import EVM.Solidity
 import EVM.Types
+import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp)
 
 import Control.Arrow ((>>>), second)
 import Data.Aeson (Value)
@@ -138,7 +139,7 @@ srcMap dapp contr opIndex = do
 
 findSrc :: Contract -> DappInfo -> Maybe SolcContract
 findSrc c dapp = do
-  hash <- maybeLitWord c.codehash
+  hash <- maybeLitWordSimp c.codehash
   case Map.lookup hash dapp.solcByHash of
     Just (_, v) -> Just v
     Nothing -> lookupCode c.code dapp
@@ -153,7 +154,7 @@ lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a =
     Just x -> pure x
     Nothing -> snd <$> find (compareCode c . fst) a.solcByCode
 lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let
-    code = BS.pack $ mapMaybe maybeLitByte $ V.toList c
+    code = BS.pack $ mapMaybe maybeLitByteSimp $ V.toList c
   in case snd <$> Map.lookup (keccak' (stripBytecodeMetadata code)) a.solcByHash of
     Just x -> pure x
     Nothing -> snd <$> find (compareCode code . fst) a.solcByCode
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
index 7a0c8a9ce..2351773ff 100644
--- a/src/EVM/Expr.hs
+++ b/src/EVM/Expr.hs
@@ -15,6 +15,7 @@ import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128))
 import Data.List
+import Data.Map qualified as LMap
 import Data.Map.Strict qualified as Map
 import Data.Maybe (mapMaybe, isJust, fromMaybe)
 import Data.Semigroup (Any, Any(..), getAny)
@@ -297,7 +298,7 @@ readWordFromBytes (Lit idx) (ConcreteBuf bs) =
 readWordFromBytes i@(Lit idx) buf = let
     bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]]
   in if all isLitByte bytes
-     then Lit (bytesToW256 . mapMaybe maybeLitByte $ bytes)
+     then Lit (bytesToW256 . mapMaybe maybeLitByteSimp $ bytes)
      else ReadWord i buf
 readWordFromBytes idx buf = ReadWord idx buf
 
@@ -351,8 +352,8 @@ copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf
     hd = padRight (unsafeInto dstOffset) $ BS.take (unsafeInto dstOffset) dst
     sl = [readByte (Lit i) src | i <- [srcOffset .. srcOffset + (size - 1)]]
     tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst
-    in if Prelude.and . (fmap isLitByte) $ sl
-       then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByte) $ sl) <> tl
+    in if all isLitByte sl
+       then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByteSimp) $ sl) <> tl
        else CopySlice s d sz src ds
   | otherwise = CopySlice s d sz src ds
 
@@ -529,8 +530,8 @@ toList buf = case bufLength buf of
   _ -> Nothing
 
 fromList :: V.Vector (Expr Byte) -> Expr Buf
-fromList bs = case Prelude.and (fmap isLitByte bs) of
-  True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByte $ bs
+fromList bs = case all isLitByte bs of
+  True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByteSimp $ bs
   -- we want to minimize the size of the resulting expression, so we do two passes:
   --   1. write all concrete bytes to some base buffer
   --   2. write all symbolic writes on top of this buffer
@@ -1326,13 +1327,10 @@ exprToAddr _ = Nothing
 
 -- TODO: make this smarter, probably we will need to use the solver here?
 wordToAddr :: Expr EWord -> Maybe (Expr EAddr)
-wordToAddr = go . simplify
-  where
-    go :: Expr EWord -> Maybe (Expr EAddr)
-    go = \case
-      WAddr a -> Just a
-      Lit a -> Just $ LitAddr (truncateToAddr a)
-      _ -> Nothing
+wordToAddr e = case (concKeccakSimpExpr e) of
+  WAddr a -> Just a
+  Lit a -> Just $ LitAddr (truncateToAddr a)
+  _ -> Nothing
 
 litCode :: BS.ByteString -> [Expr Byte]
 litCode bs = fmap LitByte (BS.unpack bs)
@@ -1484,7 +1482,7 @@ padBytesLeft n bs
 
 joinBytes :: [Expr Byte] -> Expr EWord
 joinBytes bs
-  | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe maybeLitByte) $ bs
+  | all isLitByte bs = Lit . bytesToW256 . (mapMaybe maybeLitByteSimp) $ bs
   | otherwise = let
       bytes = padBytesLeft 32 bs
     in JoinBytes
@@ -1514,7 +1512,7 @@ numBranches (ITE _ t f) = numBranches t + numBranches f
 numBranches _ = 1
 
 allLit :: [Expr Byte] -> Bool
-allLit = Data.List.and . fmap (isLitByte)
+allLit = all isLitByte
 
 -- | True if the given expression contains any node that satisfies the
 -- input predicate
@@ -1616,3 +1614,25 @@ checkLHSConstProp a = isJust $ mapPropM_ lhsConstHelper a
 -- Commutative operators should have the constant on the LHS
 checkLHSConst :: Expr a -> Bool
 checkLHSConst a = isJust $ mapExprM_ lhsConstHelper a
+
+maybeLitByteSimp :: Expr Byte -> Maybe Word8
+maybeLitByteSimp e = case (concKeccakSimpExpr e) of
+  LitByte x -> Just x
+  _ -> Nothing
+
+maybeLitWordSimp :: Expr EWord -> Maybe W256
+maybeLitWordSimp e = case (concKeccakSimpExpr e) of
+  Lit w -> Just w
+  WAddr (LitAddr w) -> Just (into w)
+  _ -> Nothing
+
+maybeLitAddrSimp :: Expr EAddr -> Maybe Addr
+maybeLitAddrSimp e = case (concKeccakSimpExpr e) of
+  LitAddr a -> Just a
+  _ -> Nothing
+
+maybeConcStoreSimp :: Expr Storage -> Maybe (LMap.Map W256 W256)
+maybeConcStoreSimp e = case (concKeccakSimpExpr e) of
+  ConcreteStore s -> Just s
+  _ -> Nothing
+
diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
index c46c38773..53aa2fe55 100644
--- a/src/EVM/Format.hs
+++ b/src/EVM/Format.hs
@@ -38,8 +38,9 @@ import EVM (traceForest, traceForest', traceContext, cheatCode)
 import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..))
 import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation)
 import EVM.Expr qualified as Expr
-import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap)
+import EVM.Solidity (SolcContract(..), Method(..))
 import EVM.Types
+import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
 
 import Control.Arrow ((>>>))
 import Optics.Core
@@ -56,7 +57,7 @@ import Data.DoubleWord (signedWord)
 import Data.Foldable (toList)
 import Data.List (isPrefixOf, sort)
 import Data.Map qualified as Map
-import Data.Maybe (catMaybes, fromMaybe)
+import Data.Maybe (catMaybes, fromMaybe, listToMaybe)
 import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn)
 import Data.Text qualified as T
 import Data.Text.Encoding qualified as T
@@ -121,6 +122,13 @@ textValues ts (ConcreteBuf bs) =
     Left (_, _, _)   -> [formatBinary bs]
 textValues ts _ = fmap (const "<symbolic>") ts
 
+textValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
+textValue ts (ConcreteBuf bs) =
+  case runGetOrFail (getAbiSeq 1 [ts]) (fromStrict bs) of
+    Right (_, _, xs) -> fromMaybe (internalError "impossible empty list") $ listToMaybe $ textAbiValues xs
+    Left (_, _, _)   -> formatBinary bs
+textValue _ _ = "<symbolic>"
+
 parenthesise :: [Text] -> Text
 parenthesise ts = "(" <> intercalate ", " ts <> ")"
 
@@ -128,7 +136,7 @@ showValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
 showValues ts b = parenthesise $ textValues ts b
 
 showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
-showValue t b = head $ textValues [t] b
+showValue t b = textValue t b
 
 showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
 showCall ts (ConcreteBuf bs) = showValues ts $ ConcreteBuf (BS.drop 4 bs)
@@ -211,7 +219,7 @@ showTrace trace =
         [] ->
           logn
         firstTopic:restTopics ->
-          case maybeLitWord firstTopic of
+          case maybeLitWordSimp firstTopic of
             Just topic ->
               case Map.lookup topic dapp.eventMap of
                 Just (Event name _ argInfos) ->
@@ -229,7 +237,7 @@ showTrace trace =
                       -- ) anonymous;
                       let
                         sig = unsafeInto $ shiftR topic 224 :: FunctionSelector
-                        usr = case maybeLitWord t2 of
+                        usr = case maybeLitWordSimp t2 of
                           Just w ->
                             pack $ show (unsafeInto w :: Addr)
                           Nothing  ->
@@ -274,8 +282,8 @@ showTrace trace =
             where
             showTopic :: AbiType -> Expr EWord -> Text
             showTopic abiType topic =
-              case maybeLitWord (Expr.concKeccakSimpExpr topic) of
-                Just w -> head $ textValues [abiType] (ConcreteBuf (word256Bytes w))
+              case maybeLitWordSimp (Expr.concKeccakSimpExpr topic) of
+                Just w -> textValue abiType (ConcreteBuf (word256Bytes w))
                 _ -> "<symbolic>"
 
           withName :: Text -> Text -> Text
@@ -369,7 +377,7 @@ ppAddr addr alwaysShowAddr =
         case (findSrc contract ?context.info) of
           Just x -> Just (contractNamePart x.contractName)
           Nothing -> Nothing
-    label = case do litAddr <- maybeLitAddr addr
+    label = case do litAddr <- maybeLitAddrSimp addr
                     Map.lookup litAddr ?context.labels of
               Nothing -> ""
               Just l -> "[" <> "\x1b[1m" <> l <> "\x1b[0m" <> "]"
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index a9b5e4b5a..210d37a37 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -16,8 +16,9 @@ import Data.List qualified as List
 import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.String.Here
-import Data.Maybe (fromJust, fromMaybe, isJust)
+import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
 import Data.Either.Extra (fromRight')
+import Data.Foldable (fold)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Set (Set)
@@ -164,7 +165,7 @@ declareIntermediates bufs stores = do
       sorted = List.sortBy compareFst $ Map.toList $ encSs <> encBs
   decls <- mapM snd sorted
   let smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty):decls
-  pure $ foldr (<>) mempty smt2
+  pure $ fold smt2
   where
     compareFst (l, _) (r, _) = compare l r
     encodeBuf n expr = do
@@ -929,9 +930,11 @@ expandExp base expnt
 -- | Concatenates a list of bytes into a larger bitvector
 concatBytes :: [Expr Byte] -> Err Builder
 concatBytes bytes = do
-  let bytesRev = reverse bytes
-  a2 <- exprToSMT (head bytesRev)
-  foldM wrap a2 $ tail bytesRev
+  case List.uncons $ reverse bytes of
+    Nothing -> Left "unexpected empty bytes"
+    Just (h, t) -> do
+      a2 <- exprToSMT h
+      foldM wrap a2 t
   where
     wrap :: Builder -> Expr a -> Err Builder
     wrap inner byte = do
@@ -990,9 +993,14 @@ parseInteger = parseSC
 parseW8 :: SpecConstant -> Word8
 parseW8 = parseSC
 
+readOrError :: (Num a, Eq a) => ReadS a -> TS.Text -> a
+readOrError reader val = fst . headErr . reader . T.unpack . T.fromStrict $ val
+  where
+    headErr x = fromMaybe (internalError "error reading empty result") $ listToMaybe x
+
 parseSC :: (Num a, Eq a) => SpecConstant -> a
-parseSC (SCHexadecimal a) = fst . head . Numeric.readHex . T.unpack . T.fromStrict $ a
-parseSC (SCBinary a) = fst . head . Numeric.readBin . T.unpack . T.fromStrict $ a
+parseSC (SCHexadecimal a) = readOrError Numeric.readHex a
+parseSC (SCBinary a) = readOrError Numeric.readBin a
 parseSC sc = internalError $ "cannot parse: " <> show sc
 
 parseErr :: (Show a) => a -> b
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index 3b48f72aa..2670a55db 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -44,7 +44,8 @@ import EVM.Types hiding (Success)
 
 import Optics.Core
 import Optics.Operators.Unsafe
-import EVM.Effects;
+import EVM.Effects
+import EVM.Expr (maybeLitByteSimp)
 
 import Control.Applicative
 import Control.Monad
@@ -729,7 +730,7 @@ stripBytecodeMetadataSym :: [Expr Byte] -> [Expr Byte]
 stripBytecodeMetadataSym b =
   let
     concretes :: [Maybe Word8]
-    concretes = maybeLitByte <$> b
+    concretes = maybeLitByteSimp <$> b
     bzzrs :: [[Maybe Word8]]
     bzzrs = fmap (Just) . BS.unpack <$> knownBzzrPrefixes
     candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 16c312255..95db2849b 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -15,8 +15,9 @@ import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.Containers.ListUtils (nubOrd)
 import Data.DoubleWord (Word256)
-import Data.List (foldl', sortBy, sort, group)
-import Data.Maybe (fromMaybe, mapMaybe)
+import Data.List (foldl', sortBy, sort)
+import Data.List.NonEmpty qualified as NE
+import Data.Maybe (fromMaybe, mapMaybe, listToMaybe)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Map.Merge.Strict qualified as Map
@@ -44,6 +45,7 @@ import EVM.Stepper (Stepper)
 import EVM.Stepper qualified as Stepper
 import EVM.Traversals
 import EVM.Types
+import EVM.Expr (maybeConcStoreSimp)
 import GHC.Conc (getNumProcessors)
 import GHC.Generics (Generic)
 import Optics.Core
@@ -78,14 +80,14 @@ isQed (Qed _) = True
 isQed _ = False
 
 groupIssues :: [ProofResult a b c String] -> [(Integer, String)]
-groupIssues results = map (\g -> (into (length g), head g)) grouped
+groupIssues results = map (\g -> (into (length g), NE.head g)) grouped
   where
     getErr :: ProofResult a b c String -> String
     getErr (EVM.SymExec.Error k) = k
     getErr (EVM.SymExec.Unknown _) = "SMT result timeout/unknown"
     getErr _ = internalError "shouldn't happen"
     sorted = sort $ map getErr results
-    grouped = group sorted
+    grouped = NE.group sorted
 
 data VeriOpts = VeriOpts
   { simp :: Bool
@@ -652,7 +654,7 @@ verify solvers opts preState maybepost = do
 expandCex :: VM Symbolic s -> SMTCex -> SMTCex
 expandCex prestate c = c { store = Map.union c.store concretePreStore }
   where
-    concretePreStore = Map.mapMaybe (maybeConcreteStore . (.storage))
+    concretePreStore = Map.mapMaybe (maybeConcStoreSimp . (.storage))
                      . Map.filter (\v -> Expr.containsNode isConcreteStore v.storage)
                      $ (prestate.env.contracts)
     isConcreteStore = \case
@@ -952,7 +954,7 @@ formatCex cd sig m@(SMTCex _ addrs _ store blockContext txContext) = T.unlines $
     prettyBuf b = internalError $ "Unexpected symbolic buffer:\n" <> T.unpack (formatExpr b)
 
 prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
-prettyCalldata cex buf sig types = head (T.splitOn "(" sig) <> "(" <> body <> ")"
+prettyCalldata cex buf sig types = headErr errSig (T.splitOn "(" sig) <> "(" <> body <> ")"
   where
     argdata = Expr.drop 4 . Expr.simplify . defaultSymbolicValues $ subModel cex buf
     body = case decodeBuf types argdata of
@@ -961,7 +963,9 @@ prettyCalldata cex buf sig types = head (T.splitOn "(" sig) <> "(" <> body <> ")
           ConcreteBuf c -> T.pack (bsToHex c)
           _ -> err
       SAbi _ -> err
+    headErr e l = fromMaybe e $ listToMaybe l 
     err = internalError $ "unable to produce a concrete model for calldata: " <> show buf
+    errSig = internalError $ "unable to split sig: " <> show sig
 
 -- | If the expression contains any symbolic values, default them to some
 -- concrete value The intuition here is that if we still have symbolic values
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 4013d8996..a37563fca 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -1269,24 +1269,6 @@ instance Show Nibble where
 
 -- Conversions -------------------------------------------------------------------------------------
 
-maybeLitByte :: Expr Byte -> Maybe Word8
-maybeLitByte (LitByte x) = Just x
-maybeLitByte _ = Nothing
-
-maybeLitWord :: Expr EWord -> Maybe W256
-maybeLitWord (Lit w) = Just w
-maybeLitWord (WAddr (LitAddr w)) = Just (into w)
-maybeLitWord _ = Nothing
-
-maybeLitAddr :: Expr EAddr -> Maybe Addr
-maybeLitAddr (LitAddr a) = Just a
-maybeLitAddr _ = Nothing
-
-maybeConcreteStore :: Expr Storage -> Maybe (Map W256 W256)
-maybeConcreteStore (ConcreteStore s) = Just s
-maybeConcreteStore _ = Nothing
-
-
 word256 :: ByteString -> Word256
 word256 xs | BS.length xs == 1 =
   -- optimize one byte pushes
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 3a9b87c29..d8a4e2f24 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -19,6 +19,7 @@ import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
 import EVM.Stepper qualified as Stepper
+import EVM.Expr (maybeLitWordSimp)
 
 import Control.Monad (void, when, forM, forM_)
 import Control.Monad.ST (RealWorld, ST, stToIO)
@@ -338,7 +339,7 @@ formatTestLog :: (?context :: DappContext) => Map W256 Event -> Expr Log -> Mayb
 formatTestLog _ (LogEntry _ _ []) = Nothing
 formatTestLog _ (GVar _) = internalError "unexpected global variable"
 formatTestLog events (LogEntry _ args (topic:_)) =
-  case maybeLitWord topic >>= \t1 -> (Map.lookup t1 events) of
+  case maybeLitWordSimp topic >>= \t1 -> (Map.lookup t1 events) of
     Nothing -> Nothing
     Just (Event name _ argInfos) ->
       case (name <> parenthesise (abiTypeSolidity <$> argTypes)) of
@@ -374,10 +375,11 @@ formatTestLog events (LogEntry _ args (topic:_)) =
         _ -> Nothing
 
         where
+          headErr l = fromMaybe (internalError "shouldn't happen") $ listToMaybe l
           argTypes = [argType | (_, argType, NotIndexed) <- argInfos]
           unquote = Text.dropAround (\c -> c == '"' || c == '«' || c == '»')
           log_unnamed =
-            Just $ showValue (head argTypes) args
+            Just $ showValue (headErr argTypes) args
           log_named =
             let (key, val) = case take 2 (textValues argTypes args) of
                   [k, v] -> (k, v)
@@ -413,7 +415,7 @@ makeTxCall params (cd, cdProps) = do
   assign (#state % #caller) params.caller
   assign (#state % #gas) (toGas params.gasCall)
   origin <- fromMaybe (initialContract (RuntimeCode (ConcreteRuntimeCode ""))) <$> use (#env % #contracts % at params.origin)
-  let insufficientBal = maybe False (\b -> b < params.gasprice * (into params.gasCall)) (maybeLitWord origin.balance)
+  let insufficientBal = maybe False (\b -> b < params.gasprice * (into params.gasCall)) (maybeLitWordSimp origin.balance)
   when insufficientBal $ internalError "insufficient balance for gas cost"
   vm <- get
   put $ initTx vm
@@ -467,7 +469,7 @@ paramsFromRpc rpcinfo = do
                              , gaslimit
                              , baseFee
                              )
-  let ts' = fromMaybe (internalError "received unexpected symbolic timestamp via rpc") (maybeLitWord ts)
+  let ts' = fromMaybe (internalError "received unexpected symbolic timestamp via rpc") (maybeLitWordSimp ts)
   pure $ TestVMParams
     -- TODO: make this symbolic! It needs some tweaking to the way that our
     -- symbolic interpreters work to allow us to symbolically exec constructor initialization
diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs
index f3eb0487e..f7e6bdac8 100644
--- a/test/EVM/Test/BlockchainTests.hs
+++ b/test/EVM/Test/BlockchainTests.hs
@@ -10,6 +10,7 @@ import EVM.Transaction
 import EVM.UnitTest (writeTrace)
 import EVM.Types hiding (Block, Case, Env)
 import EVM.Test.Tracing (interpretWithTrace, VMTrace, compareTraces, EVMToolTraceOutput(..), decodeTraceOutputHelper)
+import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
 
 import Optics.Core
 import Control.Arrow ((***), (&&&))
@@ -235,7 +236,7 @@ checkStateFail x vm (okBal, okNonce, okData, okCode) = do
     printContracts cs = putStrLn $ Map.foldrWithKey (\k c acc ->
       acc ++ "-->" <> show k ++ " : "
                    ++ (show $ fromJust c.nonce) ++ " "
-                   ++ (show $ fromJust $ maybeLitWord c.balance) ++ " "
+                   ++ (show $ fromJust $ maybeLitWordSimp c.balance) ++ " "
                    ++ (show $ fromConcrete c.storage)
                    ++ (show $ fromConcrete c.tStorage)
         ++ "\n") "" cs
@@ -533,5 +534,5 @@ vmForCase x = do
 
 forceConcreteAddrs :: Map (Expr EAddr) Contract -> Map Addr Contract
 forceConcreteAddrs cs = Map.mapKeys
-      (fromMaybe (internalError "Internal Error: unexpected symbolic address") . maybeLitAddr)
+      (fromMaybe (internalError "Internal Error: unexpected symbolic address") . maybeLitAddrSimp)
       cs
diff --git a/test/test.hs b/test/test.hs
index 6c04a10aa..7e2fcd1d7 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -33,6 +33,7 @@ import Data.Tree (flatten)
 import Data.Typeable
 import Data.Vector qualified as V
 import Data.Word (Word8, Word64)
+import Data.Char (digitToInt)
 import GHC.Conc (getNumProcessors)
 import System.Directory
 import System.Environment
@@ -72,6 +73,7 @@ import EVM.Traversals
 import EVM.Types hiding (Env)
 import EVM.Effects
 import EVM.UnitTest (writeTrace)
+import EVM.Expr (maybeLitByteSimp)
 
 testEnv :: Env
 testEnv = Env { config = defaultConfig {
@@ -447,6 +449,24 @@ tests = testGroup "hevm"
        expr <- withDefaultSolver $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
        -- putStrLnM $ T.unpack $ formatExpr expr
        assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-wordToAddr" $ do
+       let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a"
+           store = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)])
+           expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) store
+           simpExpr = Expr.wordToAddr expr
+           simpExpr2 = Expr.concKeccakSimpExpr expr
+       assertEqualM "Expression should simplify to value." simpExpr (Just $ LitAddr 0x5842cf)
+       assertEqualM "Expression should simplify to value." simpExpr2 (Lit 0x5842cf)
+    , test "simplify-storage-wordToAddr-complex" $ do
+       let a = "000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a"
+           store = ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cf)])
+           expr = SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) store
+           writeWChain = WriteWord (Lit 0x32) (Lit 0x72) (WriteWord (Lit 0x0) expr (ConcreteBuf ""))
+           kecc = Keccak (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x20) (WriteWord (Lit 0x0) expr (writeWChain)) (ConcreteBuf ""))
+           keccAnd =  (And (Lit 1461501637330902918203684832716283019655932542975) kecc)
+           outer = And (Lit 1461501637330902918203684832716283019655932542975) (SLoad (keccAnd) (ConcreteStore (Map.fromList[(W256 1184450375068808042203882151692185743185288360635, W256 0xacab)])))
+           simp = Expr.concKeccakSimpExpr outer
+       assertEqualM "Expression should simplify to value." simp (Lit 0xacab)
     ]
   , testGroup "StorageTests"
     [ test "read-from-sstore" $ assertEqualM ""
@@ -1430,7 +1450,7 @@ tests = testGroup "hevm"
     , test "jump-into-symbolic-region" $ do
         let
           -- our initCode just jumps directly to the end
-          code = BS.pack . mapMaybe maybeLitByte $ V.toList $ assemble
+          code = BS.pack . mapMaybe maybeLitByteSimp $ V.toList $ assemble
               [ OpPush (Lit 0x85)
               , OpJump
               , OpPush (Lit 1)
@@ -4709,3 +4729,31 @@ expectedConcVals nm val = case val of
   _ -> internalError $ "unsupported Abi type " <> show nm <> " val: " <> show val <> " val type: " <> showAlter val
   where
     mkWord = word . encodeAbiValue
+
+hexStringToByteString :: String -> BS.ByteString
+hexStringToByteString hexStr
+    | odd (length hexStr) = error "Hex string has an odd length"
+    | otherwise = case traverse hexPairToByte (pairs hexStr) of
+        Just bytes -> (BS.pack bytes)
+        Nothing -> error "Invalid hex string"
+  where
+    -- Convert a pair of hex characters to a byte
+    hexPairToByte :: (Char, Char) -> Maybe Word8
+    hexPairToByte (c1, c2) = do
+        b1 <- hexCharToDigit c1
+        b2 <- hexCharToDigit c2
+        return $ fromIntegral (b1 * 16 + b2)
+
+    -- Convert a single hex character to its integer value
+    hexCharToDigit :: Char -> Maybe Int
+    hexCharToDigit c
+        | c >= '0' && c <= '9' = Just (digitToInt c)
+        | c >= 'a' && c <= 'f' = Just (digitToInt c)
+        | c >= 'A' && c <= 'F' = Just (digitToInt c)
+        | otherwise = Nothing
+
+    -- Split a string into pairs of characters
+    pairs :: [a] -> [(a, a)]
+    pairs [] = []
+    pairs (x:y:xs) = (x, y) : pairs xs
+    pairs _ = error "Unexpected odd length"