From 4820e51c53fbd397aec039c0e7378eb311d7049f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Jul 2018 08:10:14 -0700
Subject: [PATCH] n/a

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 17 ++++++++++++-----
 src/smt/theory_seq.h   |  3 +--
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9f73023e4..4f31d3dc6 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -693,8 +693,6 @@ class theory_lra::imp {
     void internalize_eq(theory_var v1, theory_var v2) {     
         enode* n1 = get_enode(v1);
         enode* n2 = get_enode(v2);
-        expr*  o1 = n1->get_owner();
-        expr*  o2 = n2->get_owner();
         app_ref term(m.mk_fresh_const("eq", a.mk_real()), m);
         scoped_internalize_state st(*this);
         st.vars().push_back(v1);
@@ -706,8 +704,12 @@ class theory_lra::imp {
         add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero()));
         add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero()));
         TRACE("arith", 
-              tout << "v" << v1 << " = " << "v" << v2 << ": "
-              << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
+              {
+                  expr*  o1 = n1->get_owner();
+                  expr*  o2 = n2->get_owner();                  
+                  tout << "v" << v1 << " = " << "v" << v2 << ": "
+                       << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";
+              });
     }
 
     void del_bounds(unsigned old_size) {
@@ -1177,7 +1179,12 @@ public:
                 const lp::lar_term& term = m_solver->get_term(wi);
                 result += term.m_v * coeff;
                 for (const auto & i : term.m_coeffs) {
-                    m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
+                    if (m_variable_values.count(i.first) > 0) {
+                        result += m_variable_values[i.first] * coeff * i.second;
+                    }
+                    else {
+                        m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
+                    }
                 }                    
             }
             else {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f32b6254b..2ee49927b 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -50,8 +50,6 @@ namespace smt {
 
         class seq_value_proc;
         
-        theory_seq_params const & m_params;
-
         // cache to track evaluations under equalities
         class eval_cache {
             eqdep_map_t             m_map;
@@ -295,6 +293,7 @@ namespace smt {
         typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set;
 
         ast_manager&               m;
+        theory_seq_params const &  m_params;
         dependency_manager         m_dm;
         solution_map               m_rep;        // unification representative.
         bool                       m_reset_cache; // invalidate cache.