diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 435c0f6b7..6d5351c25 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -52,8 +52,8 @@ namespace nlsat {
         // Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser.
         std::vector<std::vector<bool>> m_prop_dom;
 
-        assignment const&            sample() const { return m_solver.get_assignment();}
-        assignment & sample() { return m_solver.get_assignment(); }
+        assignment const&            sample() const { return m_solver.sample();}
+        assignment & sample() { return m_solver.sample(); }
 
 // max_x plays the role of n in algorith 1 of the levelwise paper.
         impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am)
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index a7ed34723..a440ce09e 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -48,8 +48,8 @@ namespace nlsat {
         bool                    m_signed_project;
         bool                    m_cell_sample;
 
-        assignment const &      sample() const { return m_solver.get_assignment(); }
-        assignment &      sample() { return m_solver.get_assignment(); }
+        assignment const &      sample() const { return m_solver.sample(); }
+        assignment &      sample() { return m_solver.sample(); }
 
         struct todo_set {
             polynomial::cache  &    m_cache;
@@ -264,7 +264,7 @@ namespace nlsat {
                 polynomial_ref f(m_pm);
                 for (unsigned i = 0; i < num_factors; i++) {
                     f = m_factors.get(i);
-                    if (is_zero(sign(f, m_solver.get_assignment(), m_am))) {
+                    if (is_zero(sign(f, m_solver.sample(), m_am))) {
                         m_zero_fs.push_back(m_factors.get(i));
                         m_is_even.push_back(false);
                     }
@@ -321,7 +321,7 @@ namespace nlsat {
                 lc = m_pm.coeff(p, x, k, reduct);
                 TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
                 if (!is_zero(lc)) {
-                    if (!::is_zero(sign(lc, m_solver.get_assignment(), m_am))) {
+                    if (!::is_zero(sign(lc, m_solver.sample(), m_am))) {
                         TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
                         return;
                     }
@@ -409,7 +409,7 @@ namespace nlsat {
                     if (max_var(p) == max)
                         elim_vanishing(p); // eliminate vanishing coefficients of max
                     if (is_const(p) || max_var(p) < max) {
-                        int s = sign(p, m_solver.get_assignment(), m_am); 
+                        int s = sign(p, m_solver.sample(), m_am); 
                         if (!is_const(p)) {
                             SASSERT(max_var(p) != null_var);
                             SASSERT(max_var(p) < max);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 6bab57f66..4ca16dd23 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -4124,11 +4124,11 @@ namespace nlsat {
         nlsat_params::collect_param_descrs(d);
     }
 
-    const assignment &solver::get_assignment() const {
+    const assignment &solver::sample() const {
         return m_imp->m_assignment;
     }
 
-    assignment &solver::get_assignment() {
+    assignment &solver::sample() {
         return m_imp->m_assignment;
     }
 
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index a3656590d..67335a2c8 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -244,8 +244,8 @@ namespace nlsat {
         // -----------------------
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
-        const assignment& get_assignment() const;
-        assignment& get_assignment(); 
+        const assignment& sample() const;
+        assignment& sample(); 
 
         void reset();
         void collect_statistics(statistics & st);