mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

include debug output

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-02-05 15:31:33 -08:00
parent f4eaa6fc98
commit c40e72aaa3
2 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_interval_set.cpp
View file

@ -663,9 +663,8 @@ namespace nlsat {
continue;
m_already_visited.setx(lidx, true, false);
js.push_back(l);
if (s->m_intervals[i].m_clause) {
if (s->m_intervals[i].m_clause)
clauses.push_back(const_cast<clause*>(s->m_intervals[i].m_clause));
}
}
for (unsigned i = 0; i < num; i++) {
literal l = s->m_intervals[i].m_justification;

6
src/nlsat/nlsat_solver.cpp
View file

@ -1273,7 +1273,7 @@ namespace nlsat {
if (include_l)
core.push_back(~l);
auto j = mk_lazy_jst(m_allocator, core.size(), core.data(), clauses.size(), clauses.data());
TRACE("nlsat_resolve", display(tout, j); display_eval(tout, j));
TRACE("nlsat_resolve", display(tout, j); display_eval(tout << "evaluated:", j));
assign(l, j);
SASSERT(value(l) == l_true);
}
@ -1384,7 +1384,9 @@ namespace nlsat {
tmp = m_ism.mk_union(curr_set, xk_set);
if (m_ism.is_full(tmp)) {
TRACE("nlsat_inf_set", tout << "infeasible set + current set = R, skip literal\n";
display(tout, cls) << "\n";);
display(tout, cls) << "\n";
m_ism.display(tout, tmp); tout << "\n";
);
R_propagate(~l, tmp, false);
continue;
}