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

Don't jump over base level

Browse source
This commit is contained in:
Jakob Rath 2022-11-28 16:14:06 +01:00
parent 1b1e310919
commit 77b4303b66
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -916,7 +916,7 @@ namespace polysat {
SASSERT(best_score < lemma_score::max()); SASSERT(best_score < lemma_score::max());
SASSERT(best_lemma); SASSERT(best_lemma);
unsigned const jump_level = best_score.jump_level(); unsigned const jump_level = std::max(best_score.jump_level(), base_level());
SASSERT(jump_level <= max_jump_level); SASSERT(jump_level <= max_jump_level);
m_conflict.reset(); m_conflict.reset();
@ -1108,6 +1108,7 @@ namespace polysat {
} }
void solver::backjump(unsigned new_level) { void solver::backjump(unsigned new_level) {
SASSERT(new_level >= base_level());
if (m_level != new_level) { if (m_level != new_level) {
LOG_H3("Backjumping to level " << new_level << " from level " << m_level); LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
pop_levels(m_level - new_level); pop_levels(m_level - new_level);