From 6d3f3f2c3528c8be6debe7fb9d4e2fd9d0336a89 Mon Sep 17 00:00:00 2001
From: Valentin Promies <valentin.promies@rwth-aachen.de>
Date: Fri, 20 Feb 2026 12:56:27 +0100
Subject: [PATCH] fix

---
 src/nlsat/nlsat_explain.cpp | 17 ++++++++++-------
 src/nlsat/nlsat_solver.cpp  |  2 +-
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 06e6e15d0..f4a04edf3 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -50,6 +50,7 @@ namespace nlsat {
         bool                    m_factor;
         bool                    m_add_all_coeffs;
         bool                    m_add_zero_disc;
+        bool                    m_linear_project;
 
         assignment const &      sample() const { return m_solver.sample(); }
         assignment &            sample() { return m_solver.sample(); }
@@ -102,6 +103,8 @@ namespace nlsat {
             m_minimize_cores   = false;
             m_add_all_coeffs   = false;
             m_add_zero_disc    = false;
+            m_linear_project   = false;
+            
         }
 
     // display helpers moved to free functions in nlsat_common.h
@@ -1144,9 +1147,9 @@ namespace nlsat {
 
         /**
          *  \brief add cell literals for the linearized projection and categorize the polynomials in ps
-         *  - ps_below will contain all polynomials from ps which have a root below m_assignment w.r.t. x
-         *  - ps_above will contain all polynomials from ps which have a root above m_assignment w.r.t. x
-         *  - ps_equal will contain at least one polynomial from ps which have a root equal to m_assignment
+         *  - ps_below will contain all polynomials from ps which have a root below sample() w.r.t. x
+         *  - ps_above will contain all polynomials from ps which have a root above sample() w.r.t. x
+         *  - ps_equal will contain at least one polynomial from ps which have a root equal to sample()
          *  - In addition, they may contain additional linear polynomials added as cell boundaries
          *  - The back elements of ps_below, ps_above, ps_equal are the polynomials used for the cell literals
          */
@@ -1159,8 +1162,8 @@ namespace nlsat {
             ps_above.reset();
             ps_equal.reset();
 
-            SASSERT(m_assignment.is_assigned(x));
-            anum const & x_val = m_assignment.value(x);
+            SASSERT(sample().is_assigned(x));
+            anum const & x_val = sample().value(x);
 
             bool           lower_inf = true,   upper_inf = true;
             scoped_anum    lower(m_am),        upper(m_am);
@@ -1177,7 +1180,7 @@ namespace nlsat {
                 roots.reset();
 
                 // Temporarily unassign x, s.t. isolate_roots does not assume p as constant.
-                m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
+                m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots);
                 unsigned num_roots = roots.size();
                 if (num_roots == 0) 
                     continue;
@@ -1298,7 +1301,7 @@ namespace nlsat {
             polynomial_ref_vector ps_above_sample(m_pm);
             polynomial_ref_vector ps_equal_sample(m_pm);
             var x = m_todo.extract_max_polys(ps);
-            if (!m_assignment.is_assigned(x)) {
+            if (!sample().is_assigned(x)) {
                 // top level projection like original
                 // we could also do a covering-style projection, sparing some resultants
                 add_lcs(ps, x);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index fdfed0d9a..30673e901 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2197,7 +2197,7 @@ namespace nlsat {
             clause.reset();
             m_lazy_clause.reset();
             m_explain.set_linear_project(true);
-            m_explain.main_operator(1, &best_literal, m_lazy_clause);
+            m_explain.compute_conflict_explanation(1, &best_literal, m_lazy_clause);
             m_explain.set_linear_project(false);
 
             for (auto l : m_lazy_clause) {