mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Bugfix for rewriter exceptions in theory_fpa. Relates to #570.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-15 19:59:08 +00:00
parent 3a6ce8f8a1
commit ee60ba824f
1 changed files with 22 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/smt/theory_fpa.cpp
View file

@ -334,23 +334,30 @@ namespace smt {
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
try {
if (m_fpa_util.is_rm(e)) {
SASSERT(m_fpa_util.is_bv2rm(e_conv));
expr_ref bv_rm(m);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
catch (rewriter_exception &)
{
m_th_rw.reset();
throw;
}
else
UNREACHABLE();
return res;
}