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 #3675

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 17:40:55 -07:00
parent afce09efe4
commit 26192e848c
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_prob.cpp
View file

@ -73,6 +73,8 @@ namespace sat {
literal lit = literal(v, !m_values[v]); literal lit = literal(v, !m_values[v]);
literal nlit = ~lit; literal nlit = ~lit;
SASSERT(is_true(lit)); SASSERT(is_true(lit));
SASSERT(lit.index() < m_use_list.size());
SASSERT(m_use_list_index.size() == m_use_list.size() + 1);
for (unsigned cls_idx : use_list(*this, lit)) { for (unsigned cls_idx : use_list(*this, lit)) {
clause_info& ci = m_clauses[cls_idx]; clause_info& ci = m_clauses[cls_idx];
ci.del(lit); ci.del(lit);
@ -114,7 +116,7 @@ namespace sat {
for (literal lit : *cls) { for (literal lit : *cls) {
m_values.reserve(lit.var()+1); m_values.reserve(lit.var()+1);
m_breaks.reserve(lit.var()+1); m_breaks.reserve(lit.var()+1);
m_use_list.reserve(lit.index()+1); m_use_list.reserve((1+lit.var())*2);
m_use_list[lit.index()].push_back(idx); m_use_list[lit.index()].push_back(idx);
} }
m_probs.reserve(n+1); m_probs.reserve(n+1);