mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix output

Browse source
This commit is contained in:
Jakob Rath 2022-08-03 10:01:54 +02:00
parent a76f977f85
commit b9588af07a
3 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/conflict.cpp
View file

@ -388,7 +388,8 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override { std::ostream& display(std::ostream& out) const override {
out << "Resolve upon " << lit << " with assignment:"; out << "Resolve upon " << lit << " with assignment:";
for (pvar v : c->vars()) for (pvar v : c->vars())
out << " " << assignment_pp(s, v, s.get_value(v), true); if (s.is_assigned(v))
out << " " << assignment_pp(s, v, s.get_value(v), true);
return out; return out;
} }
}; };

2
src/math/polysat/solver.cpp
View file

@ -1063,7 +1063,7 @@ namespace polysat {
// it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
if (m_bvars.value(lit) == l_true) { if (m_bvars.value(lit) == l_true) {
// in this case the clause is useless // in this case the clause is useless
LOG(" Clause is already true, skippping..."); LOG(" Clause is already true, skipping...");
return; return;
} }
} }

1
src/math/polysat/solver.h
View file

@ -87,6 +87,7 @@ namespace polysat {
friend class scoped_solverv; friend class scoped_solverv;
friend class test_polysat; friend class test_polysat;
friend class test_fi; friend class test_fi;
friend struct inference_resolve_with_assignment;
reslimit& m_lim; reslimit& m_lim;
params_ref m_params; params_ref m_params;