diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 3f406c70a..2c9fb2054 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -280,14 +280,12 @@ void grobner_core::del_equation(equation * eq) {
 }
 
 void grobner_core::simplify_using_to_superpose(equation& eq) {
-    bool result = false;
     bool simplified;
     TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
     do {
         simplified = false;
         for (equation* p : m_to_superpose) {
             if (simplify_source_target(p, &eq)) {
-                result = true;
                 simplified = true;
             }
             if (canceled() || eq.expr()->is_scalar()) {
@@ -297,8 +295,11 @@ void grobner_core::simplify_using_to_superpose(equation& eq) {
     }
     while (simplified && !eq.expr()->is_scalar());
 
-    TRACE("grobner", tout << "simplification result: "; display_equation(tout, eq););
+    TRACE("grobner",
+          if (simplified) { tout << "simplification result: ";  display_equation(tout, eq);}
+          else  {tout << "no simplification\n";});
 }
+           
 
 const nex* grobner_core::get_highest_monomial(const nex* e) const {
     switch (e->type()) {
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 4e9d1ae25..13a16bfda 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -179,7 +179,7 @@ private:
     void init();
     void compute_basis();
     void compute_basis_init();        
-    std::unordered_set<lpvar> grobner::get_vars_of_expr_with_opening_terms(const nex* e);
+    std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
     void display_matrix(std::ostream & out) const;
     std::ostream& display(std::ostream& out) const { return m_gc.display(out); }
     void add_row(unsigned);