Skip to content

Commit 9880fcf

Browse files
committed
missing block max size constraints
1 parent 70319be commit 9880fcf

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

ir/memory.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1706,10 +1706,10 @@ void Memory::mkAxioms(const Memory &tgt) const {
17061706
expr::mkForAll(2, vars, names,
17071707
bid1 == bid2 ||
17081708
disjoint(p1.getAddress(),
1709-
p1.blockSizeAligned().zextOrTrunc(bits_ptr_address),
1709+
p1.blockMaxSizeAligned().zextOrTrunc(bits_ptr_address),
17101710
p1.blockAlignment(),
17111711
p2.getAddress(),
1712-
p2.blockSizeAligned().zextOrTrunc(bits_ptr_address),
1712+
p2.blockMaxSizeAligned().zextOrTrunc(bits_ptr_address),
17131713
p2.blockAlignment())));
17141714
}
17151715
}

0 commit comments

Comments
 (0)