mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

comment

Browse source
This commit is contained in:
Jakob Rath 2021-09-07 11:36:45 +02:00
parent eed79df481
commit b4e14c31d0
1 changed files with 1 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -558,15 +558,8 @@ namespace polysat {
LOG_H3("resolve_bool: " << lit);
sat::bool_var const var = lit.var();
SASSERT(m_bvars.is_propagation(var));
// NOTE: boolean resolution should work normally even in bailout mode.
clause* other = m_bvars.reason(var);
// if (m_conflict.is_bailout()) {
// for (sat::literal l : *other)
// set_marks(*m_constraints.lookup(l));
// // m_conflict.push_back(other); // ???
// }
m_conflict.resolve(m_constraints, var, *other);
}