From 018cb3c734a2b12f31ecbb91e06a881eae1d99a3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 30 Sep 2025 07:42:27 -0700
Subject: [PATCH] generate more proper proof format

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_stellensatz.cpp | 11 +++--------
 src/math/lp/nla_stellensatz.h   |  6 ++++++
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp
index 05632ddb8..9154da7da 100644
--- a/src/math/lp/nla_stellensatz.cpp
+++ b/src/math/lp/nla_stellensatz.cpp
@@ -547,13 +547,14 @@ namespace nla {
             insert_monomials_from_constraint(ci);                    
 
 
+        auto &constraints = m_solver.lra().constraints();
         unsigned initial_false_constraints = m_false_constraints.size();
         for (unsigned it = 0; it < m_false_constraints.size(); ++it) {
             if (it > 10 * initial_false_constraints)
                 break;
             auto ci1 = m_false_constraints[it];
             auto const &con = constraints[ci1];
-            auto [j, coeff] = find_max_lex_monomial(con.lhs());
+            lpvar j = find_max_lex_monomial(con.lhs());
             if (j == lp::null_lpvar)
                 continue;
             auto vars = m_mon2vars[j];
@@ -987,13 +988,6 @@ namespace nla {
         multiplication_justification just{old_ci, mi, j2}; 
         // compute bounds constraints and sign of vars
         lbool sign = add_bounds(vars, just.assumptions);
-
-        #if 1
-        // just skip vacuous lemmas?
-        if (l_undef == sign)
-            return lp::null_ci;
-        #endif
-
         lp::lar_term new_lhs;
         rational new_rhs(rhs);
         for (auto const & cv : lhs) {
@@ -1168,6 +1162,7 @@ namespace nla {
             SASSERT(k < factors.size());
 
             auto v = mk_term(factors[k].first);
+
             bound_assumptions bounds{"factor = 0"};        
             bound_assumption b(v, lp::lconstraint_kind::EQ, rational(0));
             bounds.bounds.push_back(b);
diff --git a/src/math/lp/nla_stellensatz.h b/src/math/lp/nla_stellensatz.h
index df12f25c7..3991ae024 100644
--- a/src/math/lp/nla_stellensatz.h
+++ b/src/math/lp/nla_stellensatz.h
@@ -135,6 +135,7 @@ namespace nla {
             external_justification, 
             internal_justification,
             multiplication_justification,
+
             resolvent_justification,
             bound_assumptions>;
 
@@ -171,6 +172,7 @@ namespace nla {
         polynomial::manager m_pm;
 
         hashtable<multiplication, multiplication::hash, multiplication::eq> m_multiplications;
+
         hashtable<resolvent, resolvent::hash, resolvent::eq> m_resolvents;
         hashtable<ineq_sig, ineq_sig::hash, ineq_sig::eq> m_inequality_table;
 
@@ -189,12 +191,14 @@ namespace nla {
 
         // additional variables and monomials and constraints
         using term_offset = std::pair<lp::lar_term, rational>;  // term and its offset
+
         lpvar mk_monomial(svector<lp::lpvar> const& vars);
         lpvar mk_monomial(svector<lp::lpvar> const &vars, lp::lpvar j);
         lpvar mk_term(term_offset &t);
 
         void gcd_normalize(vector<std::pair<rational, lpvar>> &t, lp::lconstraint_kind k, rational &rhs);
         lp::constraint_index add_ineq(justification const& just, lp::lar_term &t, lp::lconstraint_kind k, rational const &rhs);
+
         lp::constraint_index add_ineq(justification const &just, lpvar j, lp::lconstraint_kind k,
                                       rational const &rhs);
 
@@ -206,10 +210,12 @@ namespace nla {
         lpvar add_var(bool is_int);
         lbool add_bounds(svector<lpvar> const &vars, vector<bound_assumption> &bounds);
         void saturate_constraints();
+
         void saturate_constraints2();
         void eliminate(lpvar mi);
         void ext_resolve(lpvar j, lp::constraint_index lo, lp::constraint_index hi);
         std::tuple<rational, bool, bool> compute_bound(svector<lpvar> const &vars, svector<lpvar>& quot, lpvar j, rational const& coeff, lp::constraint_index ci);
+
         lp::constraint_index saturate_multiply(lp::constraint_index con_id, lpvar j1, lpvar j2);
         
         void resolve(lpvar j, lp::constraint_index ci1, lp::constraint_index ci2);