From 77d81de03fda0fc65ee9f2c336afd9b51c5a7a33 Mon Sep 17 00:00:00 2001
From: Valentin Promies <valentin.promies@rwth-aachen.de>
Date: Fri, 6 Mar 2026 14:30:22 +0100
Subject: [PATCH] fix

---
 src/nlsat/nlsat_explain.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 8f7ca86ba..1555e2989 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1733,7 +1733,7 @@ namespace nlsat {
             
             // We call levelwise directly without normalize, simplify, elim_vanishing to preserve the original polynomials
             var max_x = max_var(m_ps);
-            bool levelwise_ok = levelwise_single_cell(m_ps, max_x, m_cache, true);
+            bool levelwise_ok = levelwise_single_cell(m_ps, max_x+1, m_cache, true); // max_x+1 because we have a full sample
             SASSERT(levelwise_ok);
             m_solver.record_levelwise_result(levelwise_ok);