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

#6935

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-10 15:52:54 +09:00
parent 4a870966ad
commit 267e9e827d
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/model/model_evaluator.cpp
View file

@ -428,11 +428,15 @@ struct evaluator_cfg : public default_rewriter_cfg {
} }
else if (!fi && m_au.is_considered_partially_interpreted(f, num, args, f_ui)) { else if (!fi && m_au.is_considered_partially_interpreted(f, num, args, f_ui)) {
fi = m_model.get_func_interp(f_ui); fi = m_model.get_func_interp(f_ui);
if (fi) { if (fi) {
var_subst vs(m, false); auto interp = fi->get_interp();
result = vs(fi->get_interp(), num, args); if (interp) {
result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args)); var_subst vs(m, false);
return BR_DONE; result = vs(fi->get_interp(), num, args);
result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args));
return BR_DONE;
}
} }
} }
else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) { else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) {