mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Current base level may be too high to deallocate clause

Browse source
This commit is contained in:
Jakob Rath 2022-11-23 16:54:58 +01:00
parent 0e32077321
commit 558fd718c0
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/constraint_manager.cpp
View file

@ -62,9 +62,11 @@ namespace polysat {
void constraint_manager::register_clause(clause* cl) { void constraint_manager::register_clause(clause* cl) {
while (m_clauses.size() <= s.base_level()) unsigned clause_level = s.base_level();
clause_level = 0; // TODO: s.base_level() may be too high, if the clause is propagated at an earlier level. For now just use 0.
while (m_clauses.size() <= clause_level)
m_clauses.push_back({}); m_clauses.push_back({});
m_clauses[s.base_level()].push_back(cl); m_clauses[clause_level].push_back(cl);
} }
void constraint_manager::store(clause* cl, bool value_propagate) { void constraint_manager::store(clause* cl, bool value_propagate) {