Method fneg

smt/expr.cpp:1262–1269

}

expr expr::fneg() const {
  if (isBV()) {
    auto signbit = bits() - 1;
    return (extract(signbit, signbit) ^ mkUInt(1, 1))
             .concat(extract(signbit - 1, 0));
  }
  return unop_fold(Z3_mk_fpa_neg);
}

expr expr::copysign(const expr &sign) const {
  auto sign_bit = sign.bits() - 1;