diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9fca9b5bc..3f46a02b7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Added
 - New solc-specific simplification rules that should make the final Props a lot more readable
+- Better BufLength and Max simplifications of Expr, and further solc-specific simplifications of Expr
 
 ## [0.52.0] - 2023-10-26
 
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
index bcb2d5877..7e5c62595 100644
--- a/src/EVM/Expr.hs
+++ b/src/EVM/Expr.hs
@@ -421,7 +421,7 @@ bufLengthEnv env useEnv buf = go (Lit 0) buf
   where
     go :: Expr EWord -> Expr Buf -> Expr EWord
     go l (ConcreteBuf b) = EVM.Expr.max l (Lit (unsafeInto . BS.length $ b))
-    go l (AbstractBuf b) = Max l (BufLength (AbstractBuf b))
+    go l (AbstractBuf b) = EVM.Expr.max l (BufLength (AbstractBuf b))
     go l (WriteWord idx _ b) = go (EVM.Expr.max l (add idx (Lit 32))) b
     go l (WriteByte idx _ b) = go (EVM.Expr.max l (add idx (Lit 1))) b
     go l (CopySlice _ dstOffset size _ dst) = go (EVM.Expr.max l (add dstOffset size)) dst
@@ -946,9 +946,7 @@ simplify e = if (mapExpr go e == e)
     go (EVM.Types.Not (EVM.Types.Not a)) = a
 
     -- Some trivial min / max eliminations
-    go (Max a b) = case (a, b) of
-                    (Lit 0, _) -> b
-                    _ -> EVM.Expr.max a b
+    go (Max a b) = EVM.Expr.max a b
     go (Min a b) = case (a, b) of
                      (Lit 0, _) -> Lit 0
                      _ -> EVM.Expr.min a b
@@ -1012,6 +1010,7 @@ simplifyProp prop =
     go (PLEq (Lit l) (Lit r)) = PBool (l <= r)
     go (PLEq a (Max b _)) | a == b = PBool True
     go (PLEq a (Max _ b)) | a == b = PBool True
+    go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)
 
     -- negations
     go (PNeg (PBool b)) = PBool (Prelude.not b)
@@ -1086,7 +1085,7 @@ flattenProps (a:ax) = case a of
 
 -- removes redundant (constant True/False) props
 remRedundantProps :: [Prop] -> [Prop]
-remRedundantProps p = collapseFalse . filter (\x -> x /= PBool True) . nubOrd $ p
+remRedundantProps p = nubOrd $ collapseFalse . filter (\x -> x /= PBool True) . nubOrd $ p
   where
     collapseFalse ps = if isJust $ find (== PBool False) ps then [PBool False] else ps
 
@@ -1285,6 +1284,8 @@ min :: Expr EWord -> Expr EWord -> Expr EWord
 min x y = normArgs Min Prelude.min x y
 
 max :: Expr EWord -> Expr EWord -> Expr EWord
+max (Lit 0) y = y
+max x (Lit 0) = x
 max x y = normArgs Max Prelude.max x y
 
 numBranches :: Expr End -> Int