From 4e72d5de436d7da565ef8908dae7e4f31d6c171b Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Sat, 7 Dec 2024 16:37:55 +0000
Subject: [PATCH] memory: make equal the src and tgt alignment of unknown
 blocks POR optimization; there's no need for >= constraint

---
 ir/memory.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ir/memory.cpp b/ir/memory.cpp
index 149a7716a..181960b32 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -1582,7 +1582,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
     state->addAxiom(
       p.isHeapAllocated().implies(p_align == align && q_align == align));
     if (!p_align.isConst() || !q_align.isConst())
-      state->addAxiom(p_align.ule(q_align));
+      state->addAxiom(p_align == q_align);
   }
   for (unsigned bid = num_nonlocals_src; bid < num_nonlocals; ++bid) {
     if (skip_bid(bid))