diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index cb3a139dd..0c6884db0 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -927,7 +927,6 @@ namespace polysat {
             m_conflict.reset();
             backjump(get_level(v) - 1);
             learn_lemma(*lemma);
-            narrow(v);
         }
     }
 
@@ -1052,15 +1051,6 @@ namespace polysat {
         pop_levels(m_level - new_level);
     }
 
-    /**
-     * placeholder for factoring/gcd common factors
-     */
-    void solver::narrow(pvar v) {
-        if (is_conflict())
-            return;
-        // TODO
-    }
-
     // Add lemma to storage
     void solver::add_clause(clause& clause) {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 2b4c7bd18..d7acd95da 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -198,7 +198,6 @@ namespace polysat {
         void decide();
         void pdecide(pvar v);
 
-        void narrow(pvar v);
         void linear_propagate();