revert Z3 rewriter.hi_fp_unspecified patch since it crashes with all recent Z3 versions
I've fixed the bug in Z3; waiting for a release
MODIFY
smt/ctx.cpp
smt/ctx.cpp
@@ -16,7 +16,8 @@ void context::init() {
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");
+ // FIXME: this needs Z3 >= 4.8.7, which hasn't been released yet
+ //Z3_global_param_set("rewriter.hi_fp_unspecified", "true");
ctx = Z3_mk_context_rc(nullptr);
}

MODIFY
tests/unit/fpbitcast.opt
tests/unit/fpbitcast.opt
@@ -5,4 +5,4 @@ Name: NaN
%v = fdiv half %a, 0.0
%r = bitcast %v to i16
-; ERROR: Timeout
+; XFAIL: Value mismatch

MODIFY
tests/unit/fpbitcast2.opt
tests/unit/fpbitcast2.opt
%r = bitcast %v to i32
=>
%r = i32 0x7f800001
+
+; XFAIL: Value mismatch

revert Z3 rewriter.hi_fp_unspecified patch since it crashes with all recent Z3 versions
I've fixed the bug in Z3; waiting for a release