diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index cb1880495..b2b61f079 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -19,16 +19,16 @@ Notes:
 #ifndef POLYNOMIAL_H_
 #define POLYNOMIAL_H_
 
-#include"mpz.h"
-#include"rational.h"
-#include"obj_ref.h"
-#include"ref_vector.h"
-#include"z3_exception.h"
-#include"scoped_numeral.h"
-#include"scoped_numeral_vector.h"
-#include"params.h"
-#include"mpbqi.h"
-#include"rlimit.h"
+#include"util/mpz.h"
+#include"util/rational.h"
+#include"util/obj_ref.h"
+#include"util/ref_vector.h"
+#include"util/z3_exception.h"
+#include"util/scoped_numeral.h"
+#include"util/scoped_numeral_vector.h"
+#include"util/params.h"
+#include"util/mpbqi.h"
+#include"util/rlimit.h"
 
 class small_object_allocator;
 
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index 28d8d761a..97c8e0e91 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -19,12 +19,12 @@ Revision History:
 #ifndef SAT_TYPES_H_
 #define SAT_TYPES_H_
 
-#include"debug.h"
-#include"approx_set.h"
-#include"lbool.h"
-#include"z3_exception.h"
-#include"common_msgs.h"
-#include"vector.h"
+#include"util/debug.h"
+#include"util/approx_set.h"
+#include"util/lbool.h"
+#include"util/z3_exception.h"
+#include"util/common_msgs.h"
+#include"util/vector.h"
 #include<iomanip>
 
 namespace sat {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index b8c5ce608..02ded6a72 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -31,6 +31,7 @@
 #include "util/lp/quick_xplain.h"
 #include "util/lp/conversion_helper.h"
 #include "util/lp/int_solver.h"
+#include "util/lp/nra_solver.h"
 
 namespace lean {
 
@@ -200,9 +201,7 @@ public:
 
     void set_status(lp_status s);
 
-    lp_status find_feasible_solution();
-   
-    void add_monomial(var_index v, svector<var_index> const& vars);
+    lp_status find_feasible_solution();   
     
     lp_status solve();
 
@@ -414,6 +413,7 @@ public:
         const impq & v = m_mpq_lar_core_solver.m_r_x[j];
         return impq_is_int(v);
     }
+
     inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }	
 	final_check_status check_int_feasibility();
 };
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index 695066048..48d957aab 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -121,6 +121,7 @@ namespace nra {
                     TRACE("arith", tout << "ex: " << idx << "\n";);
                 }
                 break;
+
             case l_undef:
                 break;
             }            
diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h
index 4bd7a64a0..cc09e24d6 100644
--- a/src/util/lp/nra_solver.h
+++ b/src/util/lp/nra_solver.h
@@ -17,7 +17,7 @@ namespace lean {
 
 namespace nra {
 
-    typedef std::unordered_map<lean::var_index, rational> nra_model_t;
+
 
     class solver {
         struct imp;