From 94edbcbf06d45c45e00fbec82cf6a0a6c09250d9 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  |  1 +
 3 files changed, 10 insertions(+), 7 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 c1a2a7fb1..0ca912254 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1072,7 +1072,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 d899f3cfe..eb75eefc4 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