Merge pull request #375 from ethereum/pleq-rewrite

PLEq -- This rewrite is actually helpful in some cases
ethereum · Sep 13, 2023 · 5d2d095 · 5d2d095
2 parents 73aeff4 + 7d0a3cb
commit 5d2d095
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
@@ -863,6 +863,8 @@ evalProp prop =
     go (PLEq (Var _) (Lit val)) | val == maxLit = PBool True
     go (PLT (Lit l) (Lit r)) = PBool (l < r)
     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
 
     -- negations
     go (PNeg (PBool b)) = PBool (Prelude.not b)