From f8942dfdee59e766d4268c4e3cb70a1bd98abf3d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Oct 2025 20:17:29 -0700
Subject: [PATCH] simplify

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nra_solver.cpp | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 63ebc133a..8f653f6c1 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -194,7 +194,7 @@ struct solver::imp {
     map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
     // Create polynomial definition for variable v used in setup_assignment_solver.
     // Side-effects: updates m_vars2mon when v is a monic variable.
-    polynomial::polynomial_ref mk_definition(unsigned v, polynomial_ref_vector const& definitions) {
+    void mk_definition(unsigned v, polynomial_ref_vector& definitions) {
         auto &pm = m_nlsat->pm();
         polynomial::polynomial_ref p(pm);
         if (m_nla_core.emons().is_monic_var(v)) {
@@ -209,19 +209,22 @@ struct solver::imp {
                 else
                     p = pm.mul(p, pv);
             }
-        } else if (lra.column_has_term(v)) {
-            for (auto const& [w, coeff] : lra.get_term(v)) {
+        }
+        else if (lra.column_has_term(v)) {
+            for (auto const &[w, coeff] : lra.get_term(v)) {
                 auto pw = definitions.get(w);
                 if (!p)
                     p = pm.mul(coeff, pw);
                 else
                     p = pm.add(p, pm.mul(coeff, pw));
             }
-        } else {
-            p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created)
         }
-        return p;
+        else {
+            p = pm.mk_polynomial(v);  // nlsat var index equals v (verified above when created)
+        }
+        definitions.push_back(p);
     }
+
     void setup_assignment_solver() {
         SASSERT(need_check());
         reset();
@@ -238,7 +241,7 @@ struct solver::imp {
             scoped_anum a(am());
             am().set(a, m_nla_core.val(v).to_mpq());
             m_values->push_back(a);
-            definitions.push_back(mk_definition(v, definitions));
+            mk_definition(v, definitions);
         }
 
         // we rely on that all information encoded into the tableau is present as a constraint.