smt: simplify add_uoverflow with constants
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -843,6 +843,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
auto full_addr = expr::mkUInt(1, 1).concat(blk_addr);
// addr + size does not overflow
+ if (!size.uge(align).isFalse())
state->addPre(full_addr.add_no_uoverflow(size_zext));
// Disjointness of block's address range with other local blocks

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -533,6 +533,12 @@ expr expr::add_no_uoverflow(const expr &rhs) const {
if (min_leading_zeros() >= 1 && rhs.min_leading_zeros() >= 1)
return true;
+ int64_t n;
+ if (isInt(n))
+ return rhs.ule(-n - 1);
+ if (rhs.isInt(n))
+ return ule(-n - 1);
+
auto bw = bits();
return (zext(1) + rhs.zext(1)).extract(bw, bw) == 0;
}

smt: simplify add_uoverflow with constants