updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/nla_order_lemmas.cpp

@@ -24,6 +24,8 @@ void order::order_lemma() {
         TRACE(nla_solver, tout << "not generating order lemmas\n";);
         return;
     }
+    if (!c().params().arith_nl_linearize())
+        return;
    
     for (auto j : c().m_to_refine) {
         if (done()) break; 

src/math/lp/nra_solver.cpp

@@ -129,6 +129,7 @@ struct solver::imp {
             }
             auto lit = add_constraint(p, ci, k);
         }
+        definitions.reset();
     }
 
     void setup_solver_terms() {
@@ -153,10 +154,10 @@ struct solver::imp {
                 continue;
             auto value = m_nla_core.val(v);
             SASSERT(value.is_int());
-            unsigned sz = m_model_bounds.size();
+            unsigned offset = m_model_bounds.size() + m_max_constraint_index;
             m_model_bounds.push_back({v, value, true});
             m_model_bounds.push_back({v, value, false});
-            m_nlsat->track_model_value(lp2nl(v), value, this + sz, this + sz + 1);
+            m_nlsat->track_model_value(lp2nl(v), value, this + offset, this + offset + 1);
         }
     }
 
@@ -174,7 +175,7 @@ struct solver::imp {
     lbool check() {
         SASSERT(need_check());
         reset();
-        vector<nlsat::assumption, false> core;
+        vector<nlsat::assumption, false> core;        
         
         smt_params_helper p(m_params);
 
@@ -250,6 +251,7 @@ struct solver::imp {
             nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
             for (auto c : core) {
                 unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
+                TRACE(nra, tout << "core index " << idx << " " << m_max_constraint_index << "\n");
                 if (idx <= m_max_constraint_index)
                     ex.push_back(idx);
                 else {
@@ -360,6 +362,7 @@ struct solver::imp {
     }
 
     nlsat::literal add_constraint(polynomial::polynomial *p, unsigned idx, lp::lconstraint_kind k) {
+        m_max_constraint_index = std::max(m_max_constraint_index, idx);
         polynomial::polynomial *ps[1] = {p};
         bool is_even[1] = {false};
         nlsat::literal lit;

src/nlsat/nlsat_solver.cpp

@@ -1871,6 +1871,7 @@ namespace nlsat {
 
 
         lbool search_check() {
+            verbose_stream() << "search check\n";
             lbool r = l_undef;
             m_stats.m_conflicts = 0;
             m_stats.m_restarts = 0;
@@ -1880,8 +1881,15 @@ namespace nlsat {
                 if (r != l_true) 
                     break; 
                 ++m_stats.m_restarts;
-                vector<std::pair<var, rational>> bounds;                
 
+                gc();
+                if (m_stats.m_restarts % 10 == 0) {
+                    if (m_reordered)
+                        restore_order();
+                    apply_reorder();
+                }
+
+                vector<std::pair<var, rational>> bounds;                
                 for (var x = 0; x < num_vars(); x++) {
                     if (is_int(x) && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) {
                         scoped_anum v(m_am), vlo(m_am);
@@ -1905,13 +1913,6 @@ namespace nlsat {
                 if (bounds.empty()) 
                     break;
 
-                gc();
-                if (m_stats.m_restarts % 10 == 0) {
-                    if (m_reordered)
-                        restore_order();
-                    apply_reorder();
-                }
-
                 init_search();
                 IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_stats.m_conflicts 
                            << " :decisions " << m_stats.m_decisions 
@@ -1925,15 +1926,18 @@ namespace nlsat {
                 if (!m_model_values.empty()) {
                     bool found = false;
                     random_gen r(++m_random_seed);
-                    auto const &[x, bound] = bounds[r(bounds.size())];
+                    auto const &[x, value] = bounds[r(bounds.size())];
-                        for (auto const &[mx, mvalue, lo, hi] : m_model_values) {
+                    for (auto const &[ext_x, mvalue, lo, hi] : m_model_values) {
-                        if (mx == x) {
+                        if (ext_x == m_perm[x]) {
+                            verbose_stream() << x << " " << ext_x << " bound: " << mvalue << " value " << value
+                                             << "\n ";
+                            TRACE(nla_solver, tout << "x" << ext_x << " bound " << mvalue << "\n");
                             polynomial_ref p(m_pm);
                             rational one(1);
                             bool is_even = false;
                             p = m_pm.mk_linear(1, &one, &x, -mvalue);  // x - mvalue
                             auto *p1 = p.get();
-                            if (mvalue < bound) {
+                            if (mvalue < value) {
                                 // assert x <= mvalue
                                 // <=>
                                 // ~ (x > mvalue)