workaround bug in Z3 FPA casts with a constant fold
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1080,6 +1080,9 @@ expr expr::toBVBool() const {
}
expr expr::float2BV() const {
+ if (auto app = isAppOf(Z3_OP_FPA_TO_FP))
+ return Z3_get_app_arg(ctx(), app, 0);
+
return unop_fold(Z3_mk_fpa_to_ieee_bv);
}
@@ -1088,7 +1091,13 @@ expr expr::float2Real() const {
}
expr expr::BV2float(const expr &type) const {
- C(type);
+ C2(type);
+ if (auto app = isAppOf(Z3_OP_FPA_TO_IEEE_BV)) {
+ expr arg = Z3_get_app_arg(ctx(), app, 0);
+ if (arg.sort() == type.sort())
+ return arg;
+ }
+
return simplify_const(Z3_mk_fpa_to_fp_bv(ctx(), ast(), type.sort()), *this);
}

MODIFY
tests/unit/fp/fneg.opt
tests/unit/fp/fneg.opt
Name: identity
+%t = fneg half %a
+ =>
%t = fneg %a
+
+
+Name: identity2
+%t = fneg <2xfloat> %a
=>
%t = fneg %a

MODIFY
tests/unit/undef.opt
tests/unit/undef.opt
@@ -6,7 +6,7 @@ Name: add undef1
Name: add undef2
-%r = add undef, %in
+%r = add i11 undef, %in
=>
%r = undef ; undef + x -> undef

workaround bug in Z3 FPA casts with a constant fold