fix copysign so it checks the 1st operand for NaN as well
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -889,15 +889,14 @@ StateValue FpBinOp::toSMT(State &s) const {
bitwise = true;
fn = [&](const expr &a, const expr &b, const Type &ty, FpRoundingMode rm) {
auto fpty = ty.getAsFloatType();
- expr fp_b = fpty->getFloat(b);
- auto isnan = fp_b.isNaN();
- auto samesign = a.isFPNegative() == b.isFPNegative();
+ auto isnan = fpty->getFloat(a).isNaN() || fpty->getFloat(b).isNaN();
+ auto copysign = a.copysign(b);
if (isnan.isFalse())
- return expr::mkIf(samesign, a, a.fneg());
+ return copysign;
- expr var = expr::mkFreshVar("#flipsign", false);
- s.addNondetVar(var);
- return expr::mkIf(expr::mkIf(isnan, var, samesign), a, a.fneg());
+ expr flip = expr::mkFreshVar("#flipsign", false);
+ s.addNondetVar(flip);
+ return expr::mkIf(isnan, expr::mkIf(flip, a, a.fneg()), copysign);
};
break;
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1114,10 +1114,6 @@ expr expr::isFPZero() const {
}
expr expr::isFPNegative() const {
- if (isBV()) {
- auto signbit = bits() - 1;
- return extract(signbit, signbit) == 1;
- }
return unop_fold(Z3_mk_fpa_is_negative);
}
@@ -1190,6 +1186,11 @@ expr expr::fneg() const {
return unop_fold(Z3_mk_fpa_neg);
}
+expr expr::copysign(const expr &sign) const {
+ auto sign_bit = sign.bits() - 1;
+ return sign.extract(sign_bit, sign_bit).concat(extract(bits() - 2, 0));
+}
+
expr expr::sqrt(const expr &rm) const {
C(rm);
return simplify_const(Z3_mk_fpa_sqrt(ctx(), rm(), ast()), *this);

MODIFY
smt/expr.h
smt/expr.h
@@ -234,6 +234,7 @@ public:
expr fdiv(const expr &rhs, const expr &rm) const;
expr fabs() const;
expr fneg() const;
+ expr copysign(const expr &sign) const;
expr sqrt(const expr &rm) const;
static expr fma(const expr &a, const expr &b, const expr &c, const expr &rm);

fix copysign so it checks the 1st operand for NaN as well