mirror of
https://github.com/Z3Prover/z3
synced 2025-07-22 04:12:05 +00:00
Fix bug in iuc_solver::get_unsat_core() that prevented clean cores
This commit is contained in:
parent
d38879e478
commit
619f681d28
1 changed files with 8 additions and 9 deletions
|
@ -215,32 +215,31 @@ void iuc_solver::reset_statistics ()
|
||||||
m_learn_core_sw.reset();
|
m_learn_core_sw.reset();
|
||||||
}
|
}
|
||||||
|
|
||||||
void iuc_solver::get_unsat_core (expr_ref_vector &core)
|
void iuc_solver::get_unsat_core (expr_ref_vector &core) {
|
||||||
{
|
|
||||||
m_solver.get_unsat_core (core);
|
m_solver.get_unsat_core (core);
|
||||||
ptr_vector<expr> _core(core.size(), core.c_ptr());
|
undo_proxies_in_core (core);
|
||||||
undo_proxies_in_core (_core);
|
|
||||||
}
|
}
|
||||||
void iuc_solver::undo_proxies_in_core (ptr_vector<expr> &r)
|
|
||||||
|
void iuc_solver::undo_proxies_in_core (expr_ref_vector &r)
|
||||||
{
|
{
|
||||||
app_ref e(m);
|
app_ref e(m);
|
||||||
expr_fast_mark1 bg;
|
expr_fast_mark1 bg;
|
||||||
for (unsigned i = 0; i < m_first_assumption; ++i) {
|
for (unsigned i = 0; i < m_first_assumption; ++i) {
|
||||||
bg.mark(m_assumptions.get(i));
|
bg.mark(m_assumptions.get(i));
|
||||||
}
|
}
|
||||||
|
|
||||||
// expand proxies
|
// expand proxies
|
||||||
unsigned j = 0;
|
unsigned j = 0;
|
||||||
for (expr* rr : r) {
|
for (expr* rr : r) {
|
||||||
// skip background assumptions
|
// skip background assumptions
|
||||||
if (bg.is_marked(rr))
|
if (bg.is_marked(rr))
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
// -- undo proxies, but only if they were introduced in check_sat
|
// -- undo proxies, but only if they were introduced in check_sat
|
||||||
if (m_is_proxied && is_proxy(rr, e)) {
|
if (m_is_proxied && is_proxy(rr, e)) {
|
||||||
SASSERT (m.is_or (e));
|
SASSERT (m.is_or (e));
|
||||||
r[j++] = e->get_arg (1);
|
r[j++] = e->get_arg (1);
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
r[j++] = rr;
|
r[j++] = rr;
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue