Skip to content

Commit 47e30f5

Browse files
committed
Oops, not concretization was missing
1 parent a577254 commit 47e30f5

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/EVM/Expr.hs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1214,7 +1214,6 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
12141214

12151215
-- Negation: ~x + 1 = 0 - x (two's complement)
12161216
go (Add (Lit 1) (Not b)) = Sub (Lit 0) b
1217-
go (Xor (Lit a) b) | a == maxLit = Not b
12181217

12191218
-- add / sub identities
12201219
go (Add a b)
@@ -1227,8 +1226,13 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
12271226
| otherwise = sub a b
12281227

12291228
-- XOR normalization
1229+
go (Xor (Lit a) b) | a == maxLit = Not b
12301230
go (Xor a b) = EVM.Expr.xor a b
12311231

1232+
-- Not concretization
1233+
go (Not a) = EVM.Expr.not a
1234+
1235+
-- EqByte
12321236
go (EqByte a b) = eqByte a b
12331237

12341238
-- SHL / SHR / SAR

0 commit comments

Comments
 (0)