mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
b68efe44af
commit
238ff78374
|
@ -168,7 +168,7 @@ namespace sat {
|
|||
aig2clauses();
|
||||
++i;
|
||||
}
|
||||
while ((force || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
|
||||
while (((force && i < 5) || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
@ -826,6 +826,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
m_rw = nullptr;
|
||||
result.push_back(g.get());
|
||||
g->inc_depth();
|
||||
TRACE("elim_uncnstr_bug", g->display(tout););
|
||||
return;
|
||||
}
|
||||
modified = false;
|
||||
|
|
|
@ -73,9 +73,9 @@ public:
|
|||
if (o == l_false) resg->assert_expr(m.mk_false());
|
||||
if (o != l_undef) result.push_back(resg.get());
|
||||
// report model
|
||||
if (g->models_enabled() && (o == l_true)) {
|
||||
if (g->models_enabled() && o == l_true) {
|
||||
model_ref abstr_model = imp.get_model();
|
||||
g->add(mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model));
|
||||
resg->add(mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue