diff --git a/contrib/cmake/src/util/lp/CMakeLists.txt b/contrib/cmake/src/util/lp/CMakeLists.txt
index ec9a2e137..75051d68c 100644
--- a/contrib/cmake/src/util/lp/CMakeLists.txt
+++ b/contrib/cmake/src/util/lp/CMakeLists.txt
@@ -19,8 +19,9 @@ z3_add_component(lp
     lp_solver_instances.cpp
     lu_instances.cpp
     matrix_instances.cpp
+    nra_solver.cpp
     permutation_matrix_instances.cpp
-	quick_xplain.cpp
+    quick_xplain.cpp
     row_eta_matrix_instances.cpp
     scaler_instances.cpp
     sparse_matrix_instances.cpp
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
new file mode 100644
index 000000000..cb47b36e5
--- /dev/null
+++ b/src/util/lp/nra_solver.cpp
@@ -0,0 +1,31 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#pragma once
+#include "util/lp/nra_solver.h"
+
+namespace lp {
+
+    struct nra_solver::imp {
+        lean::lar_solver& s;
+        imp(lean::lar_solver& s): s(s) {}
+
+        lean::final_check_status check_feasible() {
+            return lean::final_check_status::GIVEUP;
+        }
+    };
+
+    nra_solver::nra_solver(lean::lar_solver& s) {
+        m_imp = alloc(imp, s);
+    }
+
+    nra_solver::~nra_solver() {
+        dealloc(m_imp);
+    }
+
+    lean::final_check_status nra_solver::check_feasible() {
+        return m_imp->check_feasible();
+    }
+}
diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h
new file mode 100644
index 000000000..bae76b0d1
--- /dev/null
+++ b/src/util/lp/nra_solver.h
@@ -0,0 +1,47 @@
+/*
+  Copyright (c) 2017 Microsoft Corporation
+  Author: Lev Nachmanson
+*/
+
+#pragma once
+#include "util/vector.h"
+#include "util/lp/lp_settings.h"
+#include "util/lp/lar_solver.h"
+
+namespace lean {
+    class lar_solver;
+}
+
+namespace lp {
+
+    class nra_solver {
+        struct imp;
+        imp* m_imp;
+
+    public:
+
+        nra_solver(lean::lar_solver& s);
+        
+        ~nra_solver();
+
+        /*
+          \brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1]
+          The variable v is equal to the product of variables vs.
+        */
+        void add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs);
+
+        /*
+          \brief Check feasiblity of linear constraints augmented by polynomial definitions
+          that are added.
+         */
+        lean::final_check_status check_feasible();
+
+        /*
+          \brief push and pop scope. 
+          Monomial definitions are retraced when popping scope.
+        */
+        void push();
+        
+        void pop(unsigned n);
+    };
+}