From 05029c6f0321337e84cc0e346bbb9cd27a38c5c3 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 18 Feb 2026 06:33:52 -1000
Subject: [PATCH] work on nl testing

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_explain.cpp |  6 +-----
 src/nlsat/nlsat_solver.cpp  | 24 ++++++++++++++++++++----
 src/test/nlsat.cpp          |  6 ++++--
 3 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 48e23c81d..d5aadf683 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1084,7 +1084,7 @@ namespace nlsat {
          * "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection"
          * https://arxiv.org/abs/2003.00409 
          */
-        void project_cdcac(polynomial_ref_vector & ps, var max_x) {
+        void project(polynomial_ref_vector & ps, var max_x) {
             bool first = true;
             if (ps.empty())
                 return;
@@ -1142,10 +1142,6 @@ namespace nlsat {
             
         }
 
-        void project(polynomial_ref_vector & ps, var max_x) {
-            project_cdcac(ps, max_x);
-        }
-
         bool check_already_added() const {
             for (bool b : m_already_added_literal) {
                 (void)b;
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index ca7e8a2f3..b14c627c8 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1092,7 +1092,7 @@ namespace nlsat {
         }
 
         // Helper: Display unsound lemma failure information
-        void display_unsound_lemma(imp& checker, scoped_bool_vars& tr, unsigned n, literal const* cls) {
+        void display_unsound_lemma(imp& checker, scoped_bool_vars& tr, unsigned n, literal const* cls, lazy_justification const* jst = nullptr) {
             verbose_stream() << "\n";
             verbose_stream() << "========== UNSOUND LEMMA DETECTED ==========\n";
             verbose_stream() << "Levelwise used for this conflict: " << (m_last_conflict_used_lws ? "YES" : "NO") << "\n";
@@ -1134,10 +1134,26 @@ namespace nlsat {
                 verbose_stream() << " = " << checker.value(tlit) << "\n";
             }
             verbose_stream() << "=============================================\n";
+            if (jst) {
+                verbose_stream() << "Initial justification (lazy_justification):\n";
+                verbose_stream() << "  Num literals: " << jst->num_lits() << "\n";
+                for (unsigned i = 0; i < jst->num_lits(); ++i) {
+                    verbose_stream() << "  jst lit[" << i << "]: ";
+                    display(verbose_stream(), jst->lit(i));
+                    verbose_stream() << "\n";
+                }
+                verbose_stream() << "  Num clauses: " << jst->num_clauses() << "\n";
+                for (unsigned i = 0; i < jst->num_clauses(); ++i) {
+                    verbose_stream() << "  jst clause[" << i << "]: ";
+                    display(verbose_stream(), jst->clause(i));
+                    verbose_stream() << "\n";
+                }
+                verbose_stream() << "=============================================\n";
+            }
             verbose_stream() << "ABORTING: Unsound lemma detected!\n";
         }
 
-        void check_lemma(unsigned n, literal const* cls, assumption_set a) {
+        void check_lemma(unsigned n, literal const* cls, assumption_set a, lazy_justification const* jst = nullptr) {
             TRACE(nlsat, display(tout << "check lemma: ", n, cls) << "\n";
                   display(tout););
             
@@ -1180,7 +1196,7 @@ namespace nlsat {
                     verbose_stream() << "Dumping lemma that internal checker thinks is not a tautology:\n";
                     verbose_stream() << "Checker levelwise calls: " << checker.m_stats.m_levelwise_calls << "\n";
                     log_lemma(verbose_stream(), n, cls, true, "internal-check-fail");
-                    display_unsound_lemma(checker, tr, n, cls);
+                    display_unsound_lemma(checker, tr, n, cls, jst);
                     exit(1);
                 }
             }
@@ -2402,7 +2418,7 @@ namespace nlsat {
             if (m_check_lemmas) {
                 TRACE(nlsat, tout << "Checking lazy clause with " << m_lazy_clause.size() << " literals:\n";
                       display(tout, m_lazy_clause.size(), m_lazy_clause.data()) << "\n";);
-                check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), nullptr);
+                check_lemma(m_lazy_clause.size(), m_lazy_clause.data(), nullptr, &jst);
                 m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr));
             }
             
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index 2380d07a7..0cf3c8912 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -2505,12 +2505,14 @@ static void tst_unsound_lws_nullified2() {
 }
 
 void tst_nlsat() {
+    tst_unsound_lws_p6236();
+    std::cout << "------------------\n";
+    tst_unsound_lws_disc_zero();
+    std::cout << "------------------\n";    
     tst_unsound_lws_nullified2();
     std::cout << "------------------\n";
     tst_unsound_lws_nullified();
     std::cout << "------------------\n";
-    tst_unsound_lws_p6236();
-    std::cout << "------------------\n";
     tst_unsound_lws_ppblockterm();
     std::cout << "------------------\n";
     tst_unsound_lws_n46();