From 6752463a8c1c1088f4c1058bbbd6df73c0f6a064 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 2 Dec 2019 11:29:35 -0800 Subject: [PATCH] solving correctly a tiny smt with grobner Signed-off-by: Lev Nachmanson --- src/math/lp/nla_grobner.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index 29e72510c..11e48a299 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -146,11 +146,9 @@ private: std::ostream& display_dependency(std::ostream& out, ci_dependency*) const; void insert_to_simplify(equation *eq) { TRACE("nla_grobner", display_equation(tout, *eq);); - SASSERT(!eq->exp()->is_scalar() || to_scalar(eq->exp())->value().is_zero()); m_to_simplify.insert(eq); } void insert_to_superpose(equation *eq) { - SASSERT(!eq->exp()->is_scalar() || to_scalar(eq->exp())->value().is_zero()); SASSERT(m_nex_creator.is_simplified(eq->exp())); m_to_superpose.insert(eq); }