This rewrite is actually helpful in some cases

ethereum · Sep 7, 2023 · 7d0a3cb · 7d0a3cb
1 parent db5e472
commit 7d0a3cb
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)