Skip to content

Commit

Permalink
memory: make equal the src and tgt alignment of unknown blocks
Browse files Browse the repository at this point in the history
POR optimization; there's no need for >= constraint
  • Loading branch information
nunoplopes committed Dec 7, 2024
1 parent ea808b0 commit 4e72d5d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ir/memory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down

0 comments on commit 4e72d5d

Please sign in to comment.