diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 4bbfde7e4..e92e5629c 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -49,7 +49,6 @@ namespace nlsat {
         bool                    m_factor;
         bool                    m_add_all_coeffs;
         bool                    m_add_zero_disc;
-        bool                    m_signed_project;
         bool                    m_cell_sample;
 
 
@@ -161,7 +160,6 @@ namespace nlsat {
             m_minimize_cores   = false;
             m_add_all_coeffs   = true;
             m_add_zero_disc = true;
-            m_signed_project   = false;
         }
 
         std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
@@ -1906,10 +1904,6 @@ namespace nlsat {
         m_imp->m_add_zero_disc = f;
     }
 
-    void explain::set_signed_project(bool f) {
-        m_imp->m_signed_project = f;
-    }
-
     void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
         (*m_imp)(n, ls, result);
     }
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index e28e0f8a3..6ca08e699 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -46,7 +46,6 @@ namespace nlsat {
         void set_factor(bool f);
         void set_add_all_coeffs(bool f);
         void set_add_zero_disc(bool f);
-        void set_signed_project(bool f);
 
         /**
            \brief Given a set of literals ls[0], ... ls[n-1] s.t.
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 66da9d707..db7210c22 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -833,7 +833,6 @@ namespace qe {
             m_answer_simplify(m),
             m_trail(m),
             m_div_mc(nullptr) {
-            s.m_solver.get_explain().set_signed_project(true);
             m_nftactic = mk_tseitin_cnf_tactic(m);
         }