From 317fed1062889c4d7e8fcd42c63f502f082e2181 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 17 Mar 2023 23:25:07 +0100 Subject: [PATCH] assertion was too strong --- src/math/polysat/solver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 6e9262582..745ec2661 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1042,7 +1042,11 @@ namespace polysat { void solver::revert_bool_decision(sat::literal const lit) { unsigned max_jump_level = m_bvars.level(lit) - 1; backjump_and_learn(max_jump_level, true); - SASSERT(m_level < max_jump_level || m_bvars.is_false(lit)); + // NOTE: happens in 42448.smt2; but does not seem to be a bug. + // we have a correct lemma but when going through the narrow queue, narrowing causes a conflict. + // thus we exit backjump_and_learn before we have a chance to propagate that lemma. + // so the assertion should hold if !is_conflict. + SASSERT(is_conflict() || m_level < max_jump_level || m_bvars.is_false(lit)); } std::optional solver::compute_lemma_score(clause const& lemma) {