From ee60ba824f0a116ec0bb5e9e615dd4fe2e9802db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 15 Nov 2016 19:59:08 +0000 Subject: [PATCH] Bugfix for rewriter exceptions in theory_fpa. Relates to #570. --- src/smt/theory_fpa.cpp | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 89acc0ecf..4b53c1341 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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; }