From b6f07e2a234914e624a0b5036ca0495241bdf1af Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 12 Aug 2018 13:04:12 +0800
Subject: [PATCH] roll back changes in get_model

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/CMakeLists.txt         | 2 +-
 src/smt/theory_lra.cpp     | 6 +++---
 src/util/lp/lar_solver.cpp | 2 --
 src/util/lp/nra_solver.cpp | 4 ++--
 4 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 53f5e1549..31dff1715 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -97,7 +97,7 @@ add_subdirectory(tactic/portfolio)
 add_subdirectory(opt)
 add_subdirectory(api)
 add_subdirectory(api/dll)
-
+add_definitions(-DDUMP_ARGS)
 ################################################################################
 # libz3
 ################################################################################
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 425770c30..216bcd559 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1489,7 +1489,7 @@ public:
         }
             
         lp::var_index vi = m_theory_var2var_index[v];
-        if (vi < m_variable_values.size())
+        if (m_variable_values.count(vi) > 0)
             return m_variable_values[vi];
         
         if (!m_solver->is_term(vi)) {
@@ -1505,7 +1505,7 @@ public:
             if (m_solver->is_term(wi)) {
                 const lp::lar_term& term = m_solver->get_term(wi);
                 for (const auto & i : term) {
-                    if (i.var() < m_variable_values.size()) {
+                    if (m_variable_values.count(i.var()) > 0) {
                         result += m_variable_values[i.var()] * coeff * i.coeff();
                     }
                     else {
@@ -1517,7 +1517,7 @@ public:
                 result += m_variable_values[wi] * coeff;
             }
         }
-        m_term_values[vi] = result;
+        m_variable_values[vi] = result;
         return result;
     }
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index da25e9648..7ee280a49 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1252,8 +1252,6 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 
 void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
     lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
-    if (m_status != lp_status::OPTIMAL)
-        return;
     mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
     unsigned i;
     unsigned n = m_mpq_lar_core_solver.m_r_x.size();
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index a4d452bee..200bdd2bc 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -29,8 +29,8 @@ namespace nra {
         scoped_ptr<scoped_anum>    m_zero;
         vector<mon_eq>         m_monomials;
         unsigned_vector        m_monomials_lim;
-        mutable vector<rational> m_variable_values; // current model        
-        mutable std::unordered_map<lp::var_index, rational> m_term_values;
+        mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model        
+
         imp(lp::lar_solver& s, reslimit& lim, params_ref const& p): 
             s(s), 
             m_limit(lim),