From 24f3cddaaccbeffe348089282da8793107a86b5a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 10 Feb 2026 13:24:52 -1000
Subject: [PATCH] relax a too strong assert

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_explain.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 06b4a38e1..dcc79bc2a 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1755,9 +1755,11 @@ namespace nlsat {
                     }
 #ifdef Z3DEBUG
                     TRACE(nlsat, m_solver.display(tout, result.size(), result.data()) << "\n"; );
-                    for (literal l : result) {
-                        CTRACE(nlsat, l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
-                        SASSERT(l_true == m_solver.value(l));
+                    if (max_var(result.size(), result.data()) > 0) { // avoid checking something like that x0 = 0 & x0 > 0 with empty sample
+                        for (literal l : result) {
+                            CTRACE(nlsat, l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
+                            SASSERT(l_true == m_solver.value(l));
+                        }
                     }
 #endif                
                     break;