diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 6acc2b043..744e3ff04 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1,4 +1,4 @@
- /*++
+/*++
 Copyright (c) 2017 Microsoft Corporation
 
 Module Name:
@@ -17,6 +17,9 @@ Author:
 #include "math/grobner/pdd_solver.h"
 #include "math/dd/pdd_interval.h"
 #include "math/dd/pdd_eval.h"
+#include "ast/ast_pp.h"
+#include <fstream>
+#include <sstream>
 using namespace nla;
 
 typedef lp::lar_term term;
@@ -1062,9 +1065,18 @@ new_lemma::~new_lemma() {
     if (current().is_conflict()) {
         c.m_conflicts++;
     }
+    
+    // Dump NLA lemma as SMT2 if parameter is enabled
+    if (c.params().arith_nl_dump_lemmas()) {
+        dump_lemma_as_smt2();
+        std::cout << name << " " << (++i) << "\n" << *this;
+    }
+    
     IF_VERBOSE(4, verbose_stream() << name << "\n");
     IF_VERBOSE(4, verbose_stream() << *this << "\n");
+
     TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; );
+    std::cout << "i:" << ++i << "\n";
 }
 
 lemma& new_lemma::current() const {
@@ -1174,6 +1186,219 @@ std::ostream& new_lemma::display(std::ostream & out) const {
     }
     return out;
 }
+
+void new_lemma::dump_lemma_as_smt2() const {
+    if (!c.params().arith_nl_dump_lemmas()) return;
+    
+    static unsigned lemma_id = 0;
+    std::ostringstream filename;
+    filename << "nla_lemma_" << (++lemma_id) << ".smt2";
+    
+    std::ofstream out(filename.str());
+    if (!out.is_open()) {
+        return; // silently fail if we can't open the file
+    }
+    
+    // Delegate to the display method for actual dumping
+    c.display_new_lemma_as_smt2(out, *this);
+    
+    out.close();
+    
+    // Print notification
+    // TRACE("nl_dump", tout << "Dumped NLA lemma to " << filename.str() << std::endl;);
+}
+
+// Helper function to format rational numbers in SMT2 format
+void core::print_rational_smt2(std::ostream& out, const rational& r) const {
+    if (r.is_int()) {
+        out << r;
+    } else {
+        // Format as (/ numerator denominator) for SMT2
+        out << "(/ " << numerator(r) << " " << denominator(r) << ")";
+    }
+}
+
+// Display a lemma as SMT2 to the given output stream
+std::ostream& core::display_new_lemma_as_smt2(std::ostream& out, const new_lemma& l) const {
+    // SMT2 header
+    out << "(set-info :source |NLA lemma from Z3|)\n";
+    out << "(set-logic QF_NRA)\n";
+
+    // Collect all variables used in the lemma
+    std::unordered_set<lpvar> vars = collect_vars(l());
+
+    // Declare variables
+    for (lpvar j : vars) {
+        std::string var_name = lra.get_variable_name(j);
+        if (var_name.empty()) {
+            var_name = "x" + std::to_string(j);
+        }
+        std::string sort = "Real";
+        out << "(declare-fun " << var_name << " () " << sort << ")\n";
+    }
+
+    // Add monic definitions (nonlinear constraints)
+    std::unordered_set<lpvar> monic_vars;
+    for (lpvar j : vars) {
+        if (is_monic_var(j)) {
+            monic_vars.insert(j);
+        }
+    }
+    
+    for (lpvar j : monic_vars) {
+        const auto& m = emon(j);
+        std::string monic_var_name = lra.get_variable_name(j);
+        if (monic_var_name.empty()) monic_var_name = "x" + std::to_string(j);
+        
+        out << "(assert ; monic definition\n  (= " << monic_var_name << " ";
+        
+        if (m.vars().size() == 0) {
+            out << "1"; // empty product = 1
+        } else if (m.vars().size() == 1) {
+            lpvar factor_var = m.vars()[0];
+            std::string factor_name = lra.get_variable_name(factor_var);
+            if (factor_name.empty()) factor_name = "x" + std::to_string(factor_var);
+            out << factor_name;
+        } else {
+            out << "(* ";
+            bool first_factor = true;
+            for (lpvar factor_var : m.vars()) {
+                if (!first_factor) out << " ";
+                first_factor = false;
+                std::string factor_name = lra.get_variable_name(factor_var);
+                if (factor_name.empty()) factor_name = "x" + std::to_string(factor_var);
+                out << factor_name;
+            }
+            out << ")";
+        }
+        out << "))\n";
+    }
+
+    // Add explanation constraints as assumptions
+    for (auto p : l().expl()) {
+        out << "(assert ; explanation constraint " << p.ci() << "\n  ";
+        const auto& constraint = lra.constraints()[p.ci()];
+        out << "(";
+        // Comparison operator
+        switch (constraint.kind()) {
+            case llc::LE: out << "<="; break;
+            case llc::LT: out << "<"; break;
+            case llc::GE: out << ">="; break;
+            case llc::GT: out << ">"; break;
+            case llc::EQ: out << "="; break;
+            case llc::NE: out << "distinct"; break;
+            default: out << "unknown_cmp"; break;
+        }
+        out << " ";
+        auto coeffs = constraint.coeffs();
+        if (coeffs.empty()) {
+            out << "0";
+        } else if (coeffs.size() == 1) {
+            const auto& coeff_var = coeffs[0];
+            std::string var_name = lra.get_variable_name(coeff_var.second);
+            if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.second);
+            if (coeff_var.first == rational::one()) {
+                out << var_name;
+            } else {
+                out << "(* ";
+                print_rational_smt2(out, coeff_var.first);
+                out << " " << var_name << ")";
+            }
+        } else {
+            out << "(+ ";
+            bool first_term = true;
+            for (const auto& coeff_var : coeffs) {
+                if (!first_term) out << " ";
+                first_term = false;
+                std::string var_name = lra.get_variable_name(coeff_var.second);
+                if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.second);
+                if (coeff_var.first == rational::one()) {
+                    out << var_name;
+                } else if (coeff_var.first == rational::minus_one()) {
+                    out << "(- " << var_name << ")";
+                } else {
+                    out << "(* ";
+                    print_rational_smt2(out, coeff_var.first);
+                    out << " " << var_name << ")";
+                }
+            }
+            out << ")";
+        }
+        // Free coefficient
+        rational free_coeff = constraint.get_free_coeff_of_left_side();
+        if (!free_coeff.is_zero()) {
+            out << " + ";
+            print_rational_smt2(out, free_coeff);
+        }
+        // Right side
+        out << " ";
+        print_rational_smt2(out, constraint.rhs());
+        out << ")\n";
+        out << ")\n";
+    }
+
+    // Add lemma as a negated assertion (to check unsatisfiability)
+    if (l().ineqs().empty()) {
+        out << "(assert false)\n";
+    } else {
+        out << "(assert (not (or\n";
+        bool first = true;
+        for (auto const& ineq : l().ineqs()) {
+            if (!first) out << "\n";
+            first = false;
+            out << "  (";
+            switch (ineq.cmp()) {
+                case llc::LE: out << "<="; break;
+                case llc::LT: out << "<"; break;
+                case llc::GE: out << ">="; break;
+                case llc::GT: out << ">"; break;
+                case llc::EQ: out << "="; break;
+                case llc::NE: out << "distinct"; break;
+                default: out << "unknown_cmp"; break;
+            }
+            out << " ";
+            if (ineq.term().size() == 0) {
+                out << "0";
+            } else if (ineq.term().size() == 1) {
+                const auto& coeff_var = *ineq.term().begin();
+                std::string var_name = lra.get_variable_name(coeff_var.j());
+                if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.j());
+                if (coeff_var.coeff() == rational::one()) {
+                    out << var_name;
+                } else {
+                    out << "(* ";
+                    print_rational_smt2(out, coeff_var.coeff());
+                    out << " " << var_name << ")";
+                }
+            } else {
+                out << "(+ ";
+                bool first_term = true;
+                for (const auto& coeff_var : ineq.term()) {
+                    if (!first_term) out << " ";
+                    first_term = false;
+                    std::string var_name = lra.get_variable_name(coeff_var.j());
+                    if (var_name.empty()) var_name = "x" + std::to_string(coeff_var.j());
+                    if (coeff_var.coeff() == rational::one()) {
+                        out << var_name;
+                    } else if (coeff_var.coeff() == rational::minus_one()) {
+                        out << "(- " << var_name << ")";
+                    } else {
+                        out << "(* ";
+                        print_rational_smt2(out, coeff_var.coeff());
+                        out << " " << var_name << ")";
+                    }
+                }
+                out << ")";
+            }
+            out << " ";
+            print_rational_smt2(out, ineq.rs());
+            out << ")";
+        }
+        out << ")))\n";
+    }
+    out << "(check-sat)\n(exit)\n";
+    return out;
+}
     
 void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
     SASSERT(val(j) != a);
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 955adeb07..28e71363c 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -241,6 +241,8 @@ public:
     std::ostream& print_product_with_vars(const T& m, std::ostream& out) const;
     std::ostream& print_monic_with_vars(const monic& m, std::ostream& out) const;
     std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
+    std::ostream& display_new_lemma_as_smt2(std::ostream& out, const new_lemma& l) const;
+    void print_rational_smt2(std::ostream& out, const rational& r) const;
     std::ostream& diagnose_pdd_miss(std::ostream& out);
     template <typename T>
     void trace_print_rms(const T& p, std::ostream& out);
diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h
index f0f796652..5596906ed 100644
--- a/src/math/lp/nla_types.h
+++ b/src/math/lp/nla_types.h
@@ -78,6 +78,7 @@ namespace nla {
         new_lemma(core& c, char const* name);
         ~new_lemma();
         lemma& operator()() { return current(); }
+        const lemma& operator()() const { return current(); }
         std::ostream& display(std::ostream& out) const;
         new_lemma& operator&=(lp::explanation const& e);
         new_lemma& operator&=(const monic& m);
@@ -91,6 +92,8 @@ namespace nla {
         new_lemma& explain_existing_lower_bound(lpvar j);
         new_lemma& explain_existing_upper_bound(lpvar j);    
         
+        void dump_lemma_as_smt2() const;
+        
         lp::explanation& expl() { return current().expl(); }
         
         unsigned num_ineqs() const { return current().ineqs().size(); }
diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
index c30ba85b8..44fa34257 100644
--- a/src/params/smt_params_helper.pyg
+++ b/src/params/smt_params_helper.pyg
@@ -85,6 +85,7 @@ def_module_params(module_name='smt',
 			  ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
 			  ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
 			  ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
+			  ('arith.nl.dump_lemmas', BOOL, False, 'dump nl lemmas to files in smt2 format'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),