From b09199c6e6d425e25f558b40d0039daa9f0b50b1 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 17 Oct 2025 18:08:01 -0700
Subject: [PATCH] fix an assert statement

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/levelwise.cpp     | 14 ++++++++------
 src/nlsat/nlsat_explain.cpp |  2 +-
 src/nlsat/nlsat_solver.cpp  | 22 ++++++++++++++++------
 3 files changed, 25 insertions(+), 13 deletions(-)

diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index a458d120a..e8bf55795 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -475,7 +475,7 @@ namespace nlsat {
          // add a property to m_Q if an equivalent one is not already present.
          // Equivalence: same m_prop_tag and same level; require the same poly as well.
         void add_to_Q_if_new(const property & pr, unsigned level) {
-             
+             SASSERT(pr.m_prop_tag != ord_inv || (pr.m_poly && !m_pm.is_zero(pr.m_poly)));
              for (auto const & q : to_vector(m_Q[level])) {
                  if (q.m_prop_tag != pr.m_prop_tag) continue;
                  if (q.m_poly != pr.m_poly) continue;
@@ -800,12 +800,9 @@ or
                     // nothing is added
                 } else {
                     polynomial_ref res = resultant(polynomial_ref(I.l, m_pm), p.m_poly, m_level);
-                    if (res) {
+                    if (m_pm.is_zero(res)) { m_fail = true; return;}
                         // Factor the resultant and add ord_inv for each distinct non-constant factor
-                        for_each_distinct_factor(res, [&](polynomial::polynomial_ref f) {
-                            mk_prop(prop_enum::ord_inv, f);
-                        });
-                    }
+                    for_each_distinct_factor(res, [&](polynomial::polynomial_ref f) { mk_prop(prop_enum::ord_inv, f);});
                 }
             } else {
             /*
@@ -920,8 +917,13 @@ or
                  poly *a = m_rel.m_rfunc[pair.first].ire.p;
                  poly *b = m_rel.m_rfunc[pair.second].ire.p;
                  SASSERT(max_var(a) == max_var(b) && max_var(b) == m_level) ;
+                 
                  polynomial_ref r(m_pm);
                  r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level);
+                 if (m_pm.is_zero(r)) {
+                     m_fail = true;
+                     return;
+                 }
                  TRACE(lws, tout << "resultant of (" << pair.first << "," << pair.second << "):"; 
                        ::nlsat::display(tout, m_solver, a) << "\n";
                        ::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n");
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 1af4bbbdc..6c1a75936 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1156,7 +1156,7 @@ namespace nlsat {
                     m_todo.reset();
                     break;
                 }
-            TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x); 
+                TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x); 
                 tout << "\npolynomials\n";
                 display(tout, m_solver, ps); tout << "\n";);
                 add_lcs(ps, x);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 546049dbf..2b1b5e86f 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1,3 +1,4 @@
+// int tttt = 0;
 /*++
 Copyright (c) 2012 Microsoft Corporation
 
@@ -1116,8 +1117,9 @@ namespace nlsat {
         }
 
         void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
-            ++m_lemma_count;
-            out << "(set-logic NRA)\n";
+            // ++tttt;
+            // if (tttt != 5225555) return;
+            out << "(set-logic NIA)\n";
             if (is_valid) {
                 display_smt2_bool_decls(out);
                 display_smt2_arith_decls(out);
@@ -1126,10 +1128,14 @@ namespace nlsat {
                 display_smt2(out);            
             for (unsigned i = 0; i < n; ++i) 
                 display_smt2(out << "(assert ", ~cls[i]) << ")\n";
-            display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n";
+            display(out << "(echo \"#" << m_lemma_count++ /*tttt*/ << " ", n, cls) << "\")\n";
             out << "(check-sat)\n(reset)\n";
 
             TRACE(nlsat, display(tout << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n");
+            // if (tttt == 5223333) {
+            //     std::cout << "exit\n";
+            //     exit(1);               
+            // }
         }
 
         clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
@@ -2200,6 +2206,13 @@ namespace nlsat {
         }
         
         void resolve_lazy_justification(bool_var b, lazy_justification const & jst) {
+            // if (tttt == 52133333) {
+            //     enable_trace("nlsat");
+            //     enable_trace("nlsat_solver");
+            //     enable_trace("nlsat_explain");
+            //     enable_trace("lws");
+            //     enable_trace("nlsat_resolve");
+            // }
             TRACE(nlsat_resolve, tout << "resolving lazy_justification for b" << b << "\n";);
             unsigned sz = jst.num_lits();
 
@@ -2211,9 +2224,6 @@ namespace nlsat {
                 print_out_as_math(verbose_stream(), jst) << std::endl;
 //                verbose_stream() << "\nend of assignment lemma\n";
             }
-
-            
-            
             
             m_lazy_clause.reset();
             m_explain.compute_conflict_explanation(jst.num_lits(), jst.lits(), m_lazy_clause);