bvSubNoUnderflow function

Expr bvSubNoUnderflow(
  1. Expr t1,
  2. Expr t2, {
  3. required bool signed,
})

Implementation

Expr bvSubNoUnderflow(Expr t1, Expr t2, {required bool signed}) {
  if (signed) {
    final zero = getSort<BitVecSort>(t1).zero();
    final minusT2 = bvNeg(t2);
    final x = bvSlt(zero, t2);
    final y = bvAddNoUnderflow(t1, minusT2);
    return implies(x, y);
  } else {
    return bvUle(t2, t1);
  }
}