bvSubNoOverflow function

Expr bvSubNoOverflow(
  1. Expr x,
  2. Expr y
)

Implementation

Expr bvSubNoOverflow(Expr x, Expr y) {
  final minusT2 = bvNeg(y);
  final s = getSort<BitVecSort>(y);
  final min = s.sMin();
  final a = eq(y, min);
  final zero = s.zero();
  final b = bvSlt(x, zero);
  final c = bvAddNoOverflow(x, minusT2, signed: true);
  return ifThenElse(a, b, c);
}