diff --git a/package/version b/package/version
index c21e67e6..c29f5f75 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.113
+0.1.114
diff --git a/pyproject.toml b/pyproject.toml
index 30b13bdd..44a23b14 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.113"
+version = "0.1.114"
 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 1dcc1499..db470824 100644
--- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
+++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
@@ -76,6 +76,9 @@ module INT-SIMPLIFICATIONS [symbolic]
   rule [int-or-bytes-2]: Bytes2Int(b"\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y, LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned)
     requires lengthBytes(Y) ==Int 2
     [simplification]
+  rule [int-or-bytes-2s]: Bytes2Int(b"\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y +Bytes b"\x00\x00", LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned)
+    requires lengthBytes(Y) ==Int 2 andBool lengthBytes(X) ==Int 2
+    [simplification]
   rule [int-or-bytes-3]: Bytes2Int(b"\x00\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y, LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned)
     requires lengthBytes(Y) ==Int 3
     [simplification]
diff --git a/src/tests/integration/test-data/specs/int-or-bytes-2s.k b/src/tests/integration/test-data/specs/int-or-bytes-2s.k
new file mode 100644
index 00000000..b7beaafc
--- /dev/null
+++ b/src/tests/integration/test-data/specs/int-or-bytes-2s.k
@@ -0,0 +1,12 @@
+module INT-OR-BYTES-2S
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1 |-> ((Bytes2Int(b"\x00\x00" +Bytes reverseBytes(substrBytes(KEY, 16, 18)), LE, Unsigned) |Int Bytes2Int(reverseBytes(substrBytes(KEY, 18, 20)) +Bytes b"\x00\x00", LE, Unsigned)) &Int 4294967295 => Bytes2Int(reverseBytes(substrBytes(KEY, 16, 20)), LE, Unsigned))
+    </regs>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires lengthBytes(KEY) ==Int 32
+endmodule
diff --git a/uv.lock b/uv.lock
index fe1f6a2b..1d1bd3ce 100644
--- a/uv.lock
+++ b/uv.lock
@@ -643,7 +643,7 @@ wheels = [
 
 [[package]]
 name = "kriscv"
-version = "0.1.113"
+version = "0.1.114"
 source = { editable = "." }
 dependencies = [
     { name = "filelock" },