mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Bugfix for FPA rewriter.
This commit is contained in:
parent
f2f6fc1994
commit
9428acd578
|
@ -143,9 +143,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
|
|||
|
||||
br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
|
||||
if (m_hi_fp_unspecified)
|
||||
result = m_util.au().mk_numeral(0, false);
|
||||
else
|
||||
// The "hardware interpretation" is 0.
|
||||
result = m_util.au().mk_numeral(rational(0), false);
|
||||
else
|
||||
result = m_util.mk_internal_to_real_unspecified();
|
||||
|
||||
return BR_DONE;
|
||||
|
|
Loading…
Reference in a new issue