Method isfloat2BV

smt/expr.cpp:643–645

}

bool expr::isfloat2BV(expr &fp) const {
  return isUnOp(fp, Z3_OP_FPA_TO_IEEE_BV);
}

unsigned expr::min_leading_zeros() const {
  expr a, b;