bvAddNoOverflow function

Expr bvAddNoOverflow(
  1. Expr x,
  2. Expr y, {
  3. required bool signed,
})

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));
  }
}