From 9a71ed87d947b259252c63b6d34fd04532d3326c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 12 Jun 2019 12:46:59 -0700
Subject: [PATCH] rebase with z3prover and fix term indices in monomials

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp   | 12 ++++++++++--
 src/math/lp/nla_core.h     |  9 ++++++---
 src/math/lp/nla_solver.cpp |  3 +--
 3 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 16afe48ad..940823cf5 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -121,8 +121,16 @@ bool core::canonize_sign(const factorization& f) const {
     return r;
 }
 
-void core::add(lpvar v, unsigned sz, lpvar const* vs) {
-    m_emons.add(v, sz, vs);
+void core::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
+    m_add_buffer.resize(sz);
+    for (unsigned i = 0; i < sz; i++) {
+        lpvar j = vs[i];
+        if (m_lar_solver.is_term(j))
+            j = m_lar_solver.adjust_term_index(j);        
+        m_add_buffer[i] = j;
+    }
+        
+    m_emons.add(v, m_add_buffer);
 }
     
 void core::push() {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 2c9f346c3..fe6ec0236 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -86,7 +86,11 @@ public:
     order                    m_order;
     monotone                 m_monotone;
     emonomials               m_emons;
-
+    svector<lpvar>            m_add_buffer;
+public:
+    emonomials& emons() { return m_emons; }
+    const emonomials& emons() const { return m_emons; }
+    // constructor
     core(lp::lar_solver& s);
 
     bool compare_holds(const rational& ls, llc cmp, const rational& rs) const;
@@ -133,8 +137,7 @@ public:
 
     void deregister_monomial_from_tables(const monomial & m, unsigned i);
 
-    // returns the monomial index
-    void add(lpvar v, unsigned sz, lpvar const* vs);   
+    void add_monomial(lpvar v, unsigned sz, lpvar const* vs);   
     void push();     
     void pop(unsigned n);
 
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index c9dbd8b06..44f3a70dd 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -27,9 +27,8 @@
 #include "math/lp/nla_intervals.h"
 namespace nla {
 
-// returns the monomial index
 void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
-    m_core->add(v, sz, vs);
+    m_core->add_monomial(v, sz, vs);
 }
 
 bool solver::is_monomial_var(lpvar v) const {