diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index 35e60a884..8a95f6ba6 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -146,9 +146,22 @@ namespace dd {
         return basic_step(pick_next());
     }
 
+    grobner::scoped_process::~scoped_process() {
+        if (e) {
+            pdd p = e->poly();
+            SASSERT(!p.is_val());
+            if (p.hi().is_val()) {
+                g.push_equation(solved, e);
+            }
+            else {
+                g.push_equation(processed, e);
+            }
+        }
+    }
+
     bool grobner::basic_step(equation* e) {
         if (!e) return false;
-        scoped_detach sd(*this, e);
+        scoped_process sd(*this, e);
         equation& eq = *e;
         TRACE("grobner", display(tout << "eq = ", eq); display(tout););
         SASSERT(eq.state() == to_simplify);
@@ -174,7 +187,7 @@ namespace dd {
     grobner::equation* grobner::pick_linear() {
         equation* eq = nullptr;
         for (auto* curr : m_to_simplify) {
-            if (!eq || curr->poly().is_linear() && is_simpler(*curr, *eq)) {
+            if (!eq || (curr->poly().is_linear() && is_simpler(*curr, *eq))) {
                 eq = curr;
             }
         }
@@ -184,8 +197,9 @@ namespace dd {
 
     void grobner::simplify() {
         try {
-            while (simplify_linear_step() /*|| simplify_cc_step() */ || simplify_elim_step()) {
+            while (simplify_linear_step(true) || simplify_linear_step(false) /*|| simplify_cc_step() */ || simplify_elim_step()) {
                 DEBUG_CODE(invariant(););
+                TRACE("grobner", display(tout););
             }
         }
         catch (pdd_manager::mem_out) {
@@ -199,11 +213,14 @@ namespace dd {
         }
     };
 
-    bool grobner::simplify_linear_step() {
+    bool grobner::simplify_linear_step(bool binary) {
         equation_vector linear;
         for (equation* e : m_to_simplify) {
-            if (e->poly().is_linear()) {
-                linear.push_back(e);
+            pdd p = e->poly();
+            if (p.is_linear()) {
+                if (!binary || p.lo().is_val() || p.lo().lo().is_val()) {
+                    linear.push_back(e);
+                }
             }
         }
         if (linear.empty()) return false;
@@ -252,7 +269,7 @@ namespace dd {
             pdd p = eq1->poly();
             auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
             equation* eq2 = e->get_data().m_value;
-            if (eq2 != eq1 && !p.lo().is_val()) {
+            if (eq2 != eq1 && p.hi().is_val() && !p.lo().is_val()) {
                 *eq1 = p - eq2->poly();
                 *eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
                 reduced = true;
@@ -495,7 +512,7 @@ namespace dd {
     bool grobner::tuned_step() {
         equation* e = tuned_pick_next();
         if (!e) return false;
-        scoped_detach sd(*this, e);
+        scoped_process sd(*this, e);
         equation& eq = *e;
         SASSERT(!m_watch[eq.poly().var()].contains(e));
         SASSERT(eq.state() == to_simplify);
diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h
index 8c8b10b39..df926c473 100644
--- a/src/math/grobner/pdd_grobner.h
+++ b/src/math/grobner/pdd_grobner.h
@@ -73,7 +73,7 @@ public:
         const pdd& poly() const { return m_poly; }        
         u_dependency * dep() const { return m_dep; }
         unsigned idx() const { return m_idx; }
-        void operator=(pdd& p) { m_poly = p; }
+        void operator=(pdd const& p) { m_poly = p; }
         void operator=(u_dependency* d) { m_dep = d; }
         eq_state state() const { return m_state; }
         void set_state(eq_state st) { m_state = st; }
@@ -160,7 +160,7 @@ private:
     void push_equation(eq_state st, equation* eq) { push_equation(st, *eq); }
 
     struct compare_top_var;
-    bool simplify_linear_step();
+    bool simplify_linear_step(bool binary);
     typedef vector<equation_vector> use_list_t;
     use_list_t get_use_list();
     void add_to_use(equation* e, use_list_t& use_list);
@@ -170,15 +170,11 @@ private:
     bool simplify_elim_step();
 
     void invariant() const;
-    struct scoped_detach {
+    struct scoped_process {
         grobner& g;
         equation* e;
-        scoped_detach(grobner& g, equation* e): g(g), e(e) {}
-        ~scoped_detach() {
-            if (e) {
-                g.push_equation(processed, *e);
-            }
-        }
+        scoped_process(grobner& g, equation* e): g(g), e(e) {}
+        ~scoped_process();        
     };
 
     void update_stats_max_degree_and_size(const equation& e);