diff --git a/src/hevm/src/EVM/Symbolic.hs b/src/hevm/src/EVM/Symbolic.hs
index 56df28bfa..760bbdc17 100644
--- a/src/hevm/src/EVM/Symbolic.hs
+++ b/src/hevm/src/EVM/Symbolic.hs
@@ -101,9 +101,9 @@ sgt (S _ x) (S _ y) =
 
 shiftRight' :: SymWord -> SymWord -> SymWord
 shiftRight' a@(S _ a') b@(S _ b') = case (num <$> unliteral a', b) of
-  (Just n, (S (FromBytes (SymbolicBuffer a)) i)) | n `mod` 8 == 0 && n <= 256 ->
+  (Just n, (S (FromBytes (StaticSymBuffer a)) i)) | n `mod` 8 == 0 && n <= 256 ->
     let bs = replicate (n `div` 8) 0 <> (take ((256 - n) `div` 8) a)
-    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
+    in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)
   _ -> sw256 $ sShiftRight b' a'
 
 -- | Operations over static symbolic memory (list of symbolic bytes)
@@ -154,7 +154,8 @@ truncpad' n m = case m of
       Nothing -> StaticSymBuffer $ takeStatic n (xs .++ literal (replicate n 0))
 
 swordAt :: Int -> [SWord 8] -> SymWord
-swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs
+swordAt i bs = let b = truncpad 32 $ drop i bs
+               in S (FromBytes (StaticSymBuffer b)) (fromBytes b)
 
 swordAt' :: SymWord -> SList (WordN 8) -> SymWord
 swordAt' i@(S _ i') bs =
@@ -213,29 +214,6 @@ readByteOrZero'' i bs =
   (bs .!! (sFromIntegral i))
   (literal 0)
 
--- Generates a ridiculously large set of constraints (roughly 25k) when
--- the index is symbolic, but it still seems (kind of) manageable
--- for the solvers.
-readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord
-readSWordWithBound ind (SymbolicBuffer xs) bound = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
-  (Just i, Just b) ->
-    let bs = truncpad 32 $ drop i (take b xs)
-    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
-  _ -> 
-    let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
-    in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
-
-readSWordWithBound ind (ConcreteBuffer xs) bound =
-  case fromSized <$> unliteral ind of
-    Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound
-    Just x' ->                                       
-       -- INVARIANT: bound should always be length xs for concrete bytes
-       -- so we should be able to safely ignore it here
-         litWord $ Concrete.readMemoryWord (num x') xs
-
-readMemoryWord' :: Word -> [SWord 8] -> SymWord
-readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m)
-
 -- pad up to 1000 bytes
 sslice :: SymWord -> SymWord -> SList (WordN 8) -> SList (WordN 8)
 sslice (S _ o) (S _ l) bs = case (unliteral $ SL.length bs, unliteral (o + l)) of
@@ -405,8 +383,13 @@ select' xs err ind = walk xs ind err
 -- for the solvers.
 readStaticWordWithBound :: SWord 32 -> ([SWord 8], SWord 32) -> SymWord
 readStaticWordWithBound ind (xs, bound) =
-  let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
-  in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
+  case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
+    (Just i, Just b) ->
+      let bs = truncpad 32 $ drop i (take b xs)
+      in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)
+    _ -> 
+      let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
+      in sw256 $ fromBytes [select' boundedList 0 (ind + j) | j <- [0..31]]
 
 -- | Custom instances for SymWord, many of which have direct
 -- analogues for concrete words defined in Concrete.hs
diff --git a/src/hevm/src/EVM/Types.hs b/src/hevm/src/EVM/Types.hs
index d2c7a97eb..421e219fb 100644
--- a/src/hevm/src/EVM/Types.hs
+++ b/src/hevm/src/EVM/Types.hs
@@ -14,6 +14,8 @@ import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..))
 #endif
 
 import Data.SBV
+import Data.SBV.List ((.++))
+import qualified Data.SBV.List as SL
 import Data.Kind
 import Data.Monoid ((<>))
 import Data.Bifunctor (first)