mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5454

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-15 19:07:37 -07:00
parent 3d13c0335f
commit 429e5ed0cd
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/fpa_solver.cpp
View file

@ -147,6 +147,8 @@ namespace fpa {
if (is_attached_to_var(n)) if (is_attached_to_var(n))
return; return;
if (m.is_ite(n->get_expr()))
return;
attach_new_th_var(n); attach_new_th_var(n);
expr* owner = n->get_expr(); expr* owner = n->get_expr();
@ -213,7 +215,10 @@ namespace fpa {
mpf_manager& mpfm = m_fpa_util.fm(); mpf_manager& mpfm = m_fpa_util.fm();
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { if (m.is_ite(n)) {
// skip
}
else if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
expr* a = nullptr, * b = nullptr, * c = nullptr; expr* a = nullptr, * b = nullptr, * c = nullptr;
if (!m_fpa_util.is_fp(n)) { if (!m_fpa_util.is_fp(n)) {
app_ref wrapped = m_converter.wrap(n); app_ref wrapped = m_converter.wrap(n);
@ -236,9 +241,6 @@ namespace fpa {
add_unit(eq_internalize(bv_val_e, n)); add_unit(eq_internalize(bv_val_e, n));
add_units(mk_side_conditions()); add_units(mk_side_conditions());
} }
else if (m.is_ite(n)) {
// pass
}
else else
add_unit(eq_internalize(m_converter.unwrap(wrapped, n->get_sort()), n)); add_unit(eq_internalize(m_converter.unwrap(wrapped, n->get_sort()), n));
} }