use Z3's fabs native encoding
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -902,7 +902,7 @@ StateValue UnaryOp::toSMT(State &s) const {
break;
case FAbs:
fn = [&](auto v, auto np) -> StateValue {
- auto f = [](expr &v) { return expr::mkIf(v.isFPNeg(), v.fneg(), v); };
+ auto f = [](expr &v) { return v.fabs(); };
return fm_poison(s, v, np, f, fmath, true);
};
break;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -947,6 +947,10 @@ expr expr::fdiv(const expr &rhs) const {
return Z3_mk_fpa_div(ctx(), rm, ast(), rhs());
}
+expr expr::fabs() const {
+ return unop_fold(Z3_mk_fpa_abs);
+}
+
expr expr::fneg() const {
return unop_fold(Z3_mk_fpa_neg);
}

MODIFY
smt/expr.h
smt/expr.h
@@ -212,6 +212,7 @@ public:
expr fsub(const expr &rhs) const;
expr fmul(const expr &rhs) const;
expr fdiv(const expr &rhs) const;
+ expr fabs() const;
expr fneg() const;
expr sqrt() const;

use Z3's fabs native encoding