mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Assertion fix for theory_fpa. Relates to #570.

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

11
src/smt/theory_fpa.cpp
View file

@ -750,8 +750,15 @@ namespace smt {
// These are the conversion functions fp.to_* */ // These are the conversion functions fp.to_* */
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
} }
else else {
UNREACHABLE(); /* Theory variables can be merged when (= bv-term (bvwrap fp-term)),
in which case context::relevant_eh may call theory_fpa::relevant_eh
after theory_bv::relevant_eh, regardless of whether theory_fpa is
interested in this term. But, this can only happen because of
(bvwrap ...) terms, i.e., `n' must be a bit-vector expression,
which we can safely ignore. */
SASSERT(m_bv_util.is_bv(n));
}
} }
void theory_fpa::reset_eh() { void theory_fpa::reset_eh() {