From e58815884ff854a2af25d90e61a1b1dd7a374566 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 4 Oct 2022 17:10:10 +0200 Subject: [PATCH] Remove debugging leftover --- src/math/polysat/solver.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 05ab96c36..0898c640d 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -930,8 +930,6 @@ namespace polysat { SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_false(lit1); })); SASSERT(all_of(lemma, [this, var](sat::literal lit1) { return var == lit1.var() || m_bvars.level(lit1) < m_bvars.level(var); })); - SASSERT(false); - m_conflict.reset(); backjump(m_bvars.level(var) - 1); learn_lemma(lemma);