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

#5420

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-20 11:20:16 -07:00
parent b84b5d091e
commit 89ed19a719
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -312,7 +312,9 @@ namespace fpa {
if (!wrapped) wrapped = m_converter.wrap(e);
return expr2enode(wrapped) != nullptr;
};
if (m_fpa_util.is_fp(e)) {
if (m_fpa_util.is_rm_numeral(e) || m_fpa_util.is_numeral(e))
value = e;
else if (m_fpa_util.is_fp(e)) {
SASSERT(n->num_args() == 3);
expr* a = values.get(n->get_arg(0)->get_root_id());
expr* b = values.get(n->get_arg(1)->get_root_id());