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

Fixed iterator invalidation bug in SAT probing. Relates to #798.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-26 14:07:05 +00:00
parent facc3215da
commit 1799310155
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/sat_probing.cpp
View file

@ -139,17 +139,17 @@ namespace sat {
if (m_probing_binary) { if (m_probing_binary) {
watch_list & wlist = s.get_wlist(~l); watch_list & wlist = s.get_wlist(~l);
watch_list::iterator it = wlist.begin(); for (unsigned i = 0; i < wlist.size(); i++) {
watch_list::iterator end = wlist.end(); watched & w = wlist[i];
for (; it != end ; ++it) { if (!w.is_binary_clause())
if (!it->is_binary_clause())
break; break;
literal l2 = it->get_literal(); literal l2 = w.get_literal();
if (l.index() > l2.index()) if (l.index() > l2.index())
continue; continue;
if (s.value(l2) != l_undef) if (s.value(l2) != l_undef)
continue; continue;
// verbose_stream() << "probing " << l << " " << l2 << " " << m_counter << "\n"; // verbose_stream() << "probing " << l << " " << l2 << " " << m_counter << "\n";
// Note: that try_lit calls propagate, which may update the watch lists.
if (!try_lit(l2, false)) if (!try_lit(l2, false))
return; return;
if (s.inconsistent()) if (s.inconsistent())