diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9fca9b5bc..9c119a220 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,8 @@ 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
+- Prop is now correctly ordered, better BufLength and Max simplifications of Expr,
+  and further solc-specific simplifications of Expr
 
 ## [0.52.0] - 2023-10-26
 
diff --git a/hevm.cabal b/hevm.cabal
index f0d617f04..feba37329 100644
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -286,7 +286,8 @@ common test-base
     optics-extra,
     witch,
     unliftio-core,
-    exceptions
+    exceptions,
+    MissingH
 
 library test-utils
   import:
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
index bcb2d5877..129b43011 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,8 @@ 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)
+    go (PLT (Lit 0) (Eq a b)) = PEq a b
 
     -- negations
     go (PNeg (PBool b)) = PBool (Prelude.not b)
@@ -1086,7 +1086,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) $ p
   where
     collapseFalse ps = if isJust $ find (== PBool False) ps then [PBool False] else ps
 
@@ -1285,6 +1285,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
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 13296066e..14a6e5eff 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -479,17 +479,30 @@ instance Ord Prop where
   PBool a <= PBool b = a <= b
   PEq (a :: Expr x) (b :: Expr x) <= PEq (c :: Expr y) (d :: Expr y)
     = case eqT @x @y of
-       Just Refl -> a <= c && b <= d
-       Nothing -> False
-  PLT a b <= PLT c d = a <= c && b <= d
-  PGT a b <= PGT c d = a <= c && b <= d
-  PGEq a b <= PGEq c d = a <= c && b <= d
-  PLEq a b <= PLEq c d = a <= c && b <= d
+       Just Refl -> a <= c || b <= d
+       Nothing -> toNum a <= toNum c
+  PLT a b <= PLT c d = a <= c || b <= d
+  PGT a b <= PGT c d = a <= c || b <= d
+  PGEq a b <= PGEq c d = a <= c || b <= d
+  PLEq a b <= PLEq c d = a <= c || b <= d
   PNeg a <= PNeg b = a <= b
-  PAnd a b <= PAnd c d = a <= c && b <= d
-  POr a b <= POr c d = a <= c && b <= d
-  PImpl a b <= PImpl c d = a <= c && b <= d
-  _ <= _ = False
+  PAnd a b <= PAnd c d = a <= c || b <= d
+  POr a b <= POr c d = a <= c || b <= d
+  PImpl a b <= PImpl c d = a <= c || b <= d
+  a <= b = asNum a <= asNum b
+    where
+      asNum :: Prop -> Int
+      asNum (PBool {}) = 0
+      asNum (PEq   {}) = 1
+      asNum (PLT   {}) = 2
+      asNum (PGT   {}) = 3
+      asNum (PGEq  {}) = 4
+      asNum (PLEq  {}) = 5
+      asNum (PNeg  {}) = 6
+      asNum (PAnd  {}) = 7
+      asNum (POr   {}) = 8
+      asNum (PImpl {}) = 9
+
 
 
 isPBool :: Prop -> Bool
diff --git a/test/test.hs b/test/test.hs
index c7d0b33bb..8296072d6 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -20,6 +20,7 @@ import Data.Binary.Get (runGetOrFail)
 import Data.DoubleWord
 import Data.Either
 import Data.List qualified as List
+import Data.List.Utils as DLU
 import Data.Map.Strict qualified as Map
 import Data.Maybe
 import Data.String.Here
@@ -44,6 +45,7 @@ import Test.Tasty.ExpectedFailure
 import Text.RE.TDFA.String
 import Text.RE.Replace
 import Witch (unsafeInto, into)
+import Data.Containers.ListUtils (nubOrd)
 
 import Optics.Core hiding (pre, re, elements)
 import Optics.State
@@ -316,6 +318,12 @@ tests = testGroup "hevm"
         let e = ReadByte (Lit 0x0) (WriteWord (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd) (Lit 0x0) (ConcreteBuf "\255\255\255\255"))
         b <- checkEquiv e (Expr.simplify e)
         assertBoolM "Simplifier failed" b
+    , test "simp-max-buflength" $ do
+      let simp = Expr.simplify $ Max (Lit 0) (BufLength (AbstractBuf "txdata"))
+      assertEqualM "max-buflength rules" simp $ BufLength (AbstractBuf "txdata")
+    , test "simp-PLT-max" $ do
+      let simp = Expr.simplifyProp $ PLT (Max (Lit 5) (BufLength (AbstractBuf "txdata"))) (Lit 99)
+      assertEqualM "max-buflength rules" simp $ PLT (BufLength (AbstractBuf "txdata")) (Lit 99)
     , test "simp-assoc-add1" $ do
       let simp = Expr.simplify $        Add (Var "a") (Add (Var "b") (Var "c"))
       assertEqualM "assoc rules" simp $ Add (Add (Var "a") (Var "b")) (Var "c")
@@ -2729,6 +2737,25 @@ tests = testGroup "hevm"
         a = successGen [PImpl (PBool False) (PEq (Var "abc") (Var "bcd"))]
         b = Expr.simplify a
       assertEqualM "Must simplify down" (successGen []) b
+    , test "propSimp-no-duplicate1" $ do
+      let a = [PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)), PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x63) (Var "arg2"),PEq (Lit 0x539) (Var "arg1"),PEq TxValue (Lit 0x0),PEq (IsZero (Eq (Lit 0x63) (Var "arg2"))) (Lit 0x0)]
+      let simp = Expr.simplifyProps a
+      assertEqualM "must not duplicate" simp (nubOrd simp)
+      assertEqualM "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp)
+    , test "propSimp-no-duplicate2" $ do
+      let a = [PNeg (PBool False),PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)),PAnd (PGEq (Var "arg2") (Lit 0x0)) (PLEq (Var "arg2") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x539) (Var "arg1"),PNeg (PEq (Lit 0x539) (Var "arg1")),PEq TxValue (Lit 0x0),PLT (BufLength (AbstractBuf "txdata")) (Lit 0x10000000000000000),PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0),PNeg (PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0)),PNeg (PEq (IsZero TxValue) (Lit 0x0))]
+      let simp = Expr.simplifyProps a
+      assertEqualM "must not duplicate" simp (nubOrd simp)
+      assertEqualM "must not duplicate" (length simp) (length $ DLU.uniq simp)
+    , test "full-order-prop1" $ do
+      let a = [PNeg (PBool False),PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)),PAnd (PGEq (Var "arg2") (Lit 0x0)) (PLEq (Var "arg2") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x539) (Var "arg1"),PNeg (PEq (Lit 0x539) (Var "arg1")),PEq TxValue (Lit 0x0),PLT (BufLength (AbstractBuf "txdata")) (Lit 0x10000000000000000),PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0),PNeg (PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0)),PNeg (PEq (IsZero TxValue) (Lit 0x0))]
+      let simp = Expr.simplifyProps a
+      assertEqualM "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp)
+    , test "full-order-prop2" $ do
+      let a =[PNeg (PBool False),PAnd (PGEq (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x44)) (PLT (Max (Lit 0x44) (BufLength (AbstractBuf "txdata"))) (Lit 0x10000000000000000)),PAnd (PGEq (Var "arg2") (Lit 0x0)) (PLEq (Var "arg2") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PAnd (PGEq (Var "arg1") (Lit 0x0)) (PLEq (Var "arg1") (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)),PEq (Lit 0x63) (Var "arg2"),PEq (Lit 0x539) (Var "arg1"),PEq TxValue (Lit 0x0),PLT (BufLength (AbstractBuf "txdata")) (Lit 0x10000000000000000),PEq (IsZero (Eq (Lit 0x63) (Var "arg2"))) (Lit 0x0),PEq (IsZero (Eq (Lit 0x539) (Var "arg1"))) (Lit 0x0),PNeg (PEq (IsZero TxValue) (Lit 0x0))]
+      let simp = Expr.simplifyProps a
+      assertEqualM "must not duplicate" simp (nubOrd simp)
+      assertEqualM "We must be able to remove all duplicates" (length $ nubOrd simp) (length $ DLU.uniq simp)
   ]
   , testGroup "equivalence-checking"
     [