mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Remove debugging leftover

Browse source
This commit is contained in:
Jakob Rath 2022-10-04 17:10:10 +02:00
parent dc9373dcbd
commit e58815884f
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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);