From c769c3b9c7ae6f24d2b3c432f4af1df404ad04c7 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 20 Dec 2024 16:38:48 +0000
Subject: [PATCH] optimize inBounds check to remove implied constraint

---
 ir/pointer.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/ir/pointer.cpp b/ir/pointer.cpp
index c659cf02b..daeec86ac 100644
--- a/ir/pointer.cpp
+++ b/ir/pointer.cpp
@@ -436,7 +436,10 @@ expr Pointer::isInboundsOf(const Pointer &block, const expr &bytes0,
 expr Pointer::isInbounds(bool strict) const {
   auto offset = getOffsetSizet();
   auto size   = blockSizeAlignedOffsetT();
-  return (strict ? offset.ult(size) : offset.ule(size)) && !offset.isNegative();
+  expr ret = strict ? offset.ult(size) : offset.ule(size);
+  if (bits_for_offset <= bits_size_t) // implied
+    ret &= !offset.isNegative();
+  return ret;
 }
 
 expr Pointer::inbounds(bool simplify_ptr) {