Set Z3's rewriter.hi_fp_unspecified=true since Z3's UF constraints dont work with quantifiers
this however forces a specific bit-pattern for NaNs, which isnt necessarily a good thing
(meaning: it allows optimizations to rely on a specific bit-pattern for all architectures)
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -14,6 +14,9 @@ void context::init() {
Z3_global_param_set("smt.ematching", "false");
Z3_global_param_set("smt.mbqi.max_iterations", "1000000");
Z3_global_param_set("timeout", get_query_timeout());
+ // Disable Z3's use of UFs for NaNs when converting FPs to BVs
+ // They generate incorrect formulas when quantifiers are involved
+ Z3_global_param_set("rewriter.hi_fp_unspecified", "true");
ctx = Z3_mk_context_rc(nullptr);
}

ADD
tests/unit/fpbitcast.opt
+Name: NaN
+%v = fdiv half %a, 0.0
+%r = bitcast %v to i16
+ =>
+%v = fdiv half %a, 0.0
+%r = bitcast %v to i16
+
+; ERROR: Timeout

ADD
tests/unit/fpbitcast2.opt
+%v = fdiv float 0.0, 0.0
+%r = bitcast %v to i32
+ =>
+%r = i32 0x7f800001

ADD
tests/unit/fpbitcast3.opt
+%v = fdiv float 0.0, 0.0
+%r = bitcast %v to i32
+ =>
+%r = i32 0x7f800002
+
+; TODO
+; XFAIL: Value mismatch

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -55,13 +55,13 @@ static void print_single_varval(ostream &os, State &st, const Model &m,
assert(n == 0);
}
- expr partial = m.eval(val.value);
+ expr partial = m.eval(val.value).simplify();
if (is_undef(partial)) {
os << "undef";
return;
}
- type.printVal(os, st, m.eval(val.value, true));
+ type.printVal(os, st, m.eval(val.value, true).simplify());
// undef variables may not have a model since each read uses a copy
// TODO: add intervals of possible values for ints at least?

Set Z3's rewriter.hi_fp_unspecified=true since Z3's UF constraints dont work with quantifiers
this however forces a specific bit-pattern for NaNs, which isnt necessarily a good thing
(meaning: it allows optimizations to rely on a specific bit-pattern for all architectures)