bvSdivNoOverflow function

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

Implementation

Expr bvSdivNoOverflow(Expr x, Expr y) {
  final s = getSort<BitVecSort>(x);
  final min = s.msb();
  final a = eq(x, min);
  final b = eq(y, bvFrom(-1, s.size));
  final u = and(a, b);
  return not(u);
}