mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

#5778

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-01 14:17:45 -07:00
parent 81084b8232
commit c7922d69ac
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_simplifier.cpp
View file

@ -1806,6 +1806,8 @@ namespace sat {
*/ */
bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) { bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) {
CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";); CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
if (m_visited.size() <= 2*s.num_vars())
m_visited.resize(2*s.num_vars(), false);
SASSERT(c1.contains(l)); SASSERT(c1.contains(l));
SASSERT(c2.contains(~l)); SASSERT(c2.contains(~l));
bool res = true; bool res = true;
@ -1825,6 +1827,10 @@ namespace sat {
literal l2 = c2[i]; literal l2 = c2[i];
if (not_l == l2) if (not_l == l2)
continue; continue;
if ((~l2).index() >= m_visited.size()) {
s.display(std::cout << l2 << " " << s.num_vars() << " " << m_visited.size() << "\n");
exit(0);
}
if (m_visited[(~l2).index()]) { if (m_visited[(~l2).index()]) {
res = false; res = false;
break; break;