From 15ebbbda2cc715728d7d5627c9cf2738bfba7e4a Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 14 Sep 2021 14:04:35 +0200 Subject: [PATCH] fix assertion --- src/math/polysat/solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d9085e5b3..0c1649422 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -743,10 +743,10 @@ namespace polysat { LOG("Lemma: " << show_deref(lemma)); for (sat::literal lit : *lemma) { LOG(" Literal " << lit << " is: " << m_constraints.lookup(lit)); - // TODO: fully evaluated constraints must be put onto the stack as propagations. signed_constraint c = m_constraints.lookup(lit); - SASSERT(m_bvars.is_assigned(lit) && !c.is_currently_false(*this)); - SASSERT(m_bvars.is_assigned(lit) && !c.is_currently_true(*this)); + // Check that fully evaluated constraints are on the stack + SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this)); + SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_true(*this)); } SASSERT(lemma->size() > 0); clause* cl = m_constraints.store(std::move(lemma));