diff --git a/package/version b/package/version
index 8b060688..1fcba8fa 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.117
+0.1.118
diff --git a/pyproject.toml b/pyproject.toml
index 99538f5f..7716c21c 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.117"
+version = "0.1.118"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"
diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
index 1a489d3d..dec09d78 100644
--- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
+++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
@@ -33,6 +33,21 @@ module INT-SIMPLIFICATIONS [symbolic]
     [simplification]
   rule [int-and-add-assoc-32]: ((X &Int 4294967295) +Int Y) &Int 4294967295 => (X +Int Y) &Int 4294967295
     [simplification]
+  rule [bytes2int-and-255]: Bytes2Int(X, LE, Unsigned) &Int 255 => Bytes2Int(X, LE, Unsigned)
+    requires lengthBytes(X) <=Int 1 [simplification]
+  rule [bytes2int-or-under-255]: Bytes2Int(b"\x00" +Bytes X, LE, Unsigned) |Int Y => Bytes2Int(Int2Bytes(Y, LE, Unsigned) +Bytes X, LE, Unsigned)
+    requires Y <Int 256 [simplification, concrete(Y)]
+```
+
+## Equality Lemmas
+
+```k
+  rule [int-eq-bytes2int]: X ==Int Bytes2Int(B0 +Bytes B1, LE, Unsigned) => 
+    (X &Int ((1 <<Int (lengthBytes(B0) *Int 8)) -Int 1)) ==Int Bytes2Int(B0, LE, Unsigned)
+    andBool
+    (X >>Int (lengthBytes(B0) *Int 8)) ==Int Bytes2Int(B1, LE, Unsigned)
+    [simplification, concrete(B0), preserves-definedness]
+    // without preserves-definedness, the rule is not applicable to B1 == substrBytes(B2, I, J)
 ```
 
 ## Inequality Lemmas
diff --git a/src/tests/integration/test-data/specs/zkevm-push.k b/src/tests/integration/test-data/specs/zkevm-push.k
new file mode 100644
index 00000000..7f04bc84
--- /dev/null
+++ b/src/tests/integration/test-data/specs/zkevm-push.k
@@ -0,0 +1,14 @@
+module ZKEVM-PUSH
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1 |-> ((Bytes2Int(OP0, LE, Unsigned) &Int 255) <<Int 8 &Int 4294967295 |Int 96 => Bytes2Int(b"`" +Bytes OP0, LE, Unsigned))
+     2 |-> (Bool2Word(239 ==Int Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) => 0)
+     3 |-> (Bool2Word(239 ==Int Bytes2Int(b"a" +Bytes substrBytes(OP1, 0, 1), LE, Unsigned)) => 0)
+    </regs>
+    <haltCond> ADDRESS(0) </haltCond>
+    requires lengthBytes(OP0) ==Int 1 andBool lengthBytes(OP1) ==Int 2
+endmodule
diff --git a/uv.lock b/uv.lock
index caf36829..c7723c7c 100644
--- a/uv.lock
+++ b/uv.lock
@@ -643,7 +643,7 @@ wheels = [
 
 [[package]]
 name = "kriscv"
-version = "0.1.117"
+version = "0.1.118"
 source = { editable = "." }
 dependencies = [
     { name = "filelock" },