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

#5336 missing theory variable creation in fpa_solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-17 20:31:11 +02:00
parent b031fefbb9
commit 6f2bf37268
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/sat/smt/q_mbi.cpp
View file

@ -168,6 +168,9 @@ namespace q {
return l_false;
if (check_forall_default(q, *qb, *mdl))
return l_false;
else {
return l_undef;
}
}
if (m_generation_bound >= m_generation_max)
return l_true;
@ -279,8 +282,9 @@ namespace q {
bool fmls_extracted = false;
TRACE("q",
tout << "Project\n";
tout << fmls << "\n";
tout << "model\n";
tout << *m_model << "\n";
tout << fmls << "\n";
tout << "model of projection\n" << mdl << "\n";
tout << "var args: " << qb.var_args.size() << "\n";
tout << "domain eqs: " << qb.domain_eqs << "\n";
@ -294,6 +298,12 @@ namespace q {
app* v = vars.get(i);
auto* p = get_plugin(v);
if (p && !fmls_extracted) {
TRACE("q", tout << "domain eqs\n" << qb.domain_eqs << "\n";);
for (expr* e : qb.domain_eqs)
if (!m_model->is_true(e))
return expr_ref(nullptr, m);
fmls.append(qb.domain_eqs);
eliminate_nested_vars(fmls, qb);
mbp::project_plugin proj(m);
@ -312,6 +322,7 @@ namespace q {
eqs.push_back(m.mk_eq(v, val));
}
rep(fmls);
TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs;);
return mk_and(fmls);
}