bvAddNoUnderflow function

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

Implementation

Expr bvAddNoUnderflow(Expr x, Expr y) {
  final zero = (getSort(x) as BitVecSort).zero();
  final r = bvAdd(x, y);
  final l1 = bvSlt(x, zero);
  final l2 = bvSlt(y, zero);
  final argsNeg = and(l1, l2);
  final lt = bvSlt(r, zero);
  return implies(argsNeg, lt);
}