diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 4d4291c2f..f69ab0bdb 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1671,7 +1671,7 @@ namespace nlsat {
             }
         }
       
-        void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
+        void compute_conflict_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) {
             SASSERT(check_already_added());
             SASSERT(num > 0);
             TRACE(nlsat_explain, 
@@ -1877,8 +1877,8 @@ namespace nlsat {
         m_imp->m_add_zero_disc = f;
     }
 
-    void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
-        (*m_imp)(n, ls, result);
+    void explain::compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result) {
+        m_imp->compute_conflict_explanation(n, ls, result);
     }
 
     void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index 6ca08e699..f423cab4a 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -64,7 +64,7 @@ namespace nlsat {
                  - s_1, ..., s_m do not contain variable x.
                  - s_1, ..., s_m are false in the current interpretation
         */
-        void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result);
+        void compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
 
         
         /**
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index 3715bf69d..a47d40867 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -320,7 +320,7 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned
 static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
     std::cout << "Project ";
     nlsat::scoped_literal_vector result(s);
-    ex.main_operator(num, lits, result);
+    ex.compute_conflict_explanation(num, lits, result);
     std::cout << "(or";
     for (auto l : result) {
         s.display(std::cout << " ", l);