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

reduce output

Browse source
This commit is contained in:
Jakob Rath 2024-05-15 10:15:25 +02:00
parent f4d5bd5cd1
commit 343d693929
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/core.cpp
View file

@ -392,7 +392,7 @@ namespace polysat {
SASSERT(!is_assigned(v)); SASSERT(!is_assigned(v));
if (!m_viable.assign(v, value, dep)) { if (!m_viable.assign(v, value, dep)) {
auto deps = m_viable.explain(); auto deps = m_viable.explain();
verbose_stream() << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n"; TRACE("bv", tout << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n");
s.set_conflict(deps, "non-viable assignment"); s.set_conflict(deps, "non-viable assignment");
return; return;
} }

2
src/sat/smt/polysat/viable.cpp
View file

@ -207,7 +207,7 @@ namespace polysat {
// display_explain(verbose_stream() << "found: ", {e,val}) << "\n"; // display_explain(verbose_stream() << "found: ", {e,val}) << "\n";
m_explain.push_back({ e, val }); m_explain.push_back({ e, val });
if (is_conflict()) { if (is_conflict()) {
verbose_stream() << "find_overlap conflict\n"; // verbose_stream() << "find_overlap conflict\n";
m_explain_kind = explain_t::conflict; m_explain_kind = explain_t::conflict;
return nullptr; return nullptr;
} }