From 2696775088d709e456a263fd4a92852932e12ffc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jul 2022 04:03:25 -0700 Subject: [PATCH] remove stale assertion with support for substitutions we allow the simplifier to change the state of equations. --- src/math/grobner/pdd_solver.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index d9171aabd..aefe5d6dc 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -200,7 +200,6 @@ namespace dd { // pushed to solved } else if (simplified && changed_leading_term) { - SASSERT(target.state() == processed); push_equation(to_simplify, target); if (!m_var2level.empty()) { m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);