diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 6b09dfbf4..1168952d4 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -378,8 +378,6 @@ namespace dd {
     inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
     inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
     inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
-    inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
-    inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
 
     inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
     inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index 992c7e784..c661ee4ef 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -698,7 +698,6 @@ namespace dd {
                 }
             }
             if (eq) {
-
                 pop_equation(eq);
                 m_watch[eq->poly().var()].erase(eq);
                 return eq;
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index 3301aa246..262e82329 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -130,7 +130,6 @@ public:
 private:
     bool step();
     equation* pick_next();
-    equation* pick_linear();
     bool canceled();
     bool done();
     void superpose(equation const& eq1, equation const& eq2);