From 80bb084611ecf754a4ebc7fd3aea382f98d4f548 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 24 May 2017 14:47:09 -0700
Subject: [PATCH] add missing initialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/lp/lar_solver.cpp | 4 +++-
 src/util/lp/nra_solver.cpp | 1 -
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index fee17dc77..97e1c102f 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -31,7 +31,9 @@ lar_solver::lar_solver() : m_status(OPTIMAL),
                            m_infeasible_column_index(-1),
                            m_terms_start_index(1000000),
                            m_mpq_lar_core_solver(m_settings, *this)
-{}
+{
+    m_nra = alloc(nra::solver, *this);
+}
     
 void lar_solver::set_propagate_bounds_on_pivoted_rows_mode(bool v) {
     m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr;
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index a5d2e671a..2308b9c45 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -30,7 +30,6 @@ namespace nra {
         vector<mon_eq>                   m_monomials;
         unsigned_vector                  m_lim;
         mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
-        vector<std::pair<rational, unsigned>> m_core;
 
         imp(lean::lar_solver& s): 
             s(s) {