diff --git a/package/version b/package/version
index 793d0e31..8b060688 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.116
+0.1.117
diff --git a/pyproject.toml b/pyproject.toml
index 9fc19311..99538f5f 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.116"
+version = "0.1.117"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"
diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md
index 69c03a6b..669d62e4 100644
--- a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md
+++ b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md
@@ -183,6 +183,13 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     [simplification]
 ```
 
+## Additional Bytes Simplifications
+
+```k
+  rule [bytes2int-pad-trailing-zeros]: Bytes2Int (B:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) => Bytes2Int (B, LE, Unsigned) 
+    [simplification(45)]
+```
+
 ```k
 endmodule
 ```
diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
index c6ed0166..008893ca 100644
--- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
+++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md
@@ -54,6 +54,10 @@ module INT-SIMPLIFICATIONS [symbolic]
 
 ```k
   rule [int-and-ineq]: 0 <=Int A &Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
+  rule [int-and-ineq-4294967295]: 0 <=Int _ &Int 4294967295 => true [simplification(45)]
+  rule [int-and-ineq-65535]: 0 <=Int _ &Int 65535 => true [simplification(45)]
+  rule [int-and-ineq-255]: 0 <=Int _ &Int 255 => true [simplification(45)]
+  rule [int-or-gt]: 0 <Int A |Int B => true requires 0 <Int A orBool 0 <Int B [simplification]
   rule [int-rhs-ineq]: 0 <=Int A >>Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
   rule [int-add-ineq]: A <=Int A +Int B => true requires 0 <=Int B [simplification]
   rule [int-add-ineq-0]: 0 <=Int A +Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
@@ -61,6 +65,15 @@ module INT-SIMPLIFICATIONS [symbolic]
     requires 0 <=Int A andBool A <=Int X [simplification]
 ```
 
+## Additional Int Simplifications
+
+```k
+  rule [int-add-ineq-pos-1]: 0 <Int A +Int B => true 
+    requires 0 <=Int A andBool 0 <Int B [simplification(45)]
+  rule [int-add-ineq-pos-2]: 0 <Int A +Int B => true 
+    requires 0 <Int A andBool 0 <=Int B [simplification]
+```
+
 ## Int Expression Simplifications for Bytes
 
 ### Shift Left for Bytes
diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/word-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/word-simplifications.md
index 6fe82807..2d3d56c7 100644
--- a/src/kriscv/kdist/riscv-semantics/lemmas/word-simplifications.md
+++ b/src/kriscv/kdist/riscv-semantics/lemmas/word-simplifications.md
@@ -19,6 +19,12 @@ module WORD-SIMPLIFICATIONS
 
 ```k
   rule [bool2word-non-neg]: 0 <=Int Bool2Word(_) => true [simplification]
+  rule [bool2word-eq-0]: Bool2Word(B) ==Int 0 => notBool B [simplification]
+  rule [bool2word-eq-1]: Bool2Word(B) ==Int 1 => B [simplification]
+
+
+  rule [int-bool2word-or-ineq]: 0 <Int (0 -Int Bool2Word(4294967295 <Int X)) &Int 4294967295 |Int X &Int 4294967295 => true 
+    requires 0 <Int X [simplification(45)]
 ```
 
 ```k
diff --git a/src/tests/integration/test-data/specs/byte-offset-bounds-check.k b/src/tests/integration/test-data/specs/byte-offset-bounds-check.k
new file mode 100644
index 00000000..161ce87c
--- /dev/null
+++ b/src/tests/integration/test-data/specs/byte-offset-bounds-check.k
@@ -0,0 +1,21 @@
+module BYTE-OFFSET-BOUNDS-CHECK
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1  |-> (Bool2Word(0 <Int (0 -Int Bool2Word(4294967295 <Int X)) &Int 4294967295 |Int X &Int 4294967295) => 1)
+     2  |-> (Bool2Word(0 <=Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned )) => 1)
+     3  |-> (Bool2Word(0 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32) => 1)
+     4  |-> (Bool2Word(0 <Int 0 -Int Bool2Word ( 4294967295 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32 ) &Int 4294967295 |Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32 &Int 4294967295) => 1)
+     // 5  |-> (Bool2Word(4294967295 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32) => 0)
+     6  |-> (Bool2Word(Y <=Int Z) => 0)
+     7  |-> (Bool2Word(Z <=Int 4294967295) => 1)
+    </regs>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires 0 <Int X 
+     andBool lengthBytes(OFFSET) ==Int 1
+     andBool notBool (Y <=Int Z)
+     andBool notBool (Bool2Word(Z <=Int 4294967295) ==Int 0)
+endmodule
diff --git a/uv.lock b/uv.lock
index 7eaaa4cc..caf36829 100644
--- a/uv.lock
+++ b/uv.lock
@@ -643,7 +643,7 @@ wheels = [
 
 [[package]]
 name = "kriscv"
-version = "0.1.116"
+version = "0.1.117"
 source = { editable = "." }
 dependencies = [
     { name = "filelock" },