mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

remove stale assertion

Browse source 
with support for substitutions we allow the simplifier to change the state of equations.
This commit is contained in:
Nikolaj Bjorner 2022-07-15 04:03:25 -07:00
parent 6688c1d62a
commit 2696775088
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/grobner/pdd_solver.cpp
View file

@ -200,7 +200,6 @@ namespace dd {
// pushed to solved // pushed to solved
} }
else if (simplified && changed_leading_term) { else if (simplified && changed_leading_term) {
SASSERT(target.state() == processed);
push_equation(to_simplify, target); push_equation(to_simplify, target);
if (!m_var2level.empty()) { if (!m_var2level.empty()) {
m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1); m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);