Function div_ub

ir/constant.cpp:134–138

}

static void div_ub(const expr &a, const expr &b, State &s, bool sign) {
  s.addPre(b != 0);
  if (sign)
    s.addPre(a != expr::IntSMin(b.bits()) || b != -1);
}

StateValue ConstantBinOp::toSMT(State &s) const {
  auto &[a, ap] = s[lhs];