diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 9074a6af41..9e2444ceab 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.643"
+version = "1.0.644"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index caaad3e3ed..e46253fd7d 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.643'
+VERSION: Final = '1.0.644'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
index b8793ee89f..d528af8986 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
@@ -87,11 +87,16 @@ module EVM-INT-SIMPLIFICATION-COMMON
   // chop
   // ###########################################################################
 
-    rule [chop-idempotent]:  chop(I) => I requires #rangeUInt( 256 , I ) [simplification]
+    rule [chop-resolve]:     chop(I) => I requires #rangeUInt( 256 , I ) [simplification]
     rule [chop-upper-bound]: 0 <=Int chop(_V)             => true        [simplification, smt-lemma]
     rule [chop-lower-bound]:         chop(_V) <Int pow256 => true        [simplification, smt-lemma]
 
     rule [chop-sum-left]:  chop ( chop ( X:Int ) +Int Y:Int ) => chop ( X +Int Y ) [simplification]
     rule [chop-sum-right]: chop ( X:Int +Int chop ( Y:Int ) ) => chop ( X +Int Y ) [simplification]
 
+    rule [chop-no-overflow-add]:
+      X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256
+      requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
+      [simplification]
+
 endmodule
diff --git a/package/version b/package/version
index b9f0f10a3e..fd0e1c0467 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.643
+1.0.644