Merge branch 'main' into overapproximate-staticcall

CHANGELOG.md

@@ -8,13 +8,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## Added
 - When a staticcall is made to a contract that does not exist, we overapproximate
   and return symbolic values
+- More simplification rules for Props
 
 ## 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

src/EVM/Expr.hs

@@ -1220,7 +1220,9 @@ simplifyProp prop =
     go (PLEq _ (Lit x)) | x == maxLit = PBool True
     go (PLT  (Lit val) (Var _)) | val == maxLit = PBool False
     go (PLEq (Var _) (Lit val)) | val == maxLit = PBool True
+    go (PLT a b) | a == b = PBool False
     go (PLT (Lit l) (Lit r)) = PBool (l < r)
+    go (PLEq a b) | a == b = PBool True
     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
@@ -1232,6 +1234,9 @@ simplifyProp prop =
     go (PNeg (PBool b)) = PBool (Prelude.not b)
     go (PNeg (PNeg a)) = a
 
+    -- Empty buf
+    go (PEq (Lit 0) (BufLength k)) = peq k (ConcreteBuf "")
+
     -- solc specific stuff
     go (PEq (Lit 0) (IsZero (IsZero (Eq a b)))) = PNeg (peq a b)