bvAddNoOverflow function
Implementation
Expr bvAddNoOverflow(Expr x, Expr y, {required bool signed}) {
if (signed) {
final zero = getSort<BitVecSort>(x).zero();
final r = bvAdd(x, y);
final l1 = bvSlt(zero, x);
final l2 = bvSlt(zero, y);
final argsPos = and(l1, l2);
final lt = bvSlt(zero, r);
return implies(argsPos, lt);
} else {
final size = getSort<BitVecSort>(x).size;
x = bvZeroExt(x, 1);
y = bvZeroExt(y, 1);
final r = bvAdd(x, y);
final ex = bvExtract(r, size, size);
return eq(ex, bvFrom(0, 1));
}
}