diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 4253f55f1..8a8c3c8f8 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1381,6 +1381,8 @@ lbool core::check() {
     TRACE(nla_solver, tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
     IF_VERBOSE(5, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
     CTRACE(nla_solver, ret == l_undef, tout << "Monomials\n"; print_monics(tout););
+    CTRACE(nla_solver, ret == l_undef, display_smt(tout););
+    // if (ret == l_undef) IF_VERBOSE(0, display_smt(verbose_stream()));
     return ret;
 }
 
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index fa5da5a81..6121a79a7 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -115,6 +115,9 @@ class core {
     bool is_pseudo_linear(monic const& m) const;    
     void refine_pseudo_linear(monic const& m);
 
+    std::ostream& display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const;
+    std::ostream& display_declarations_smt(std::ostream& out) const;
+
 public:    
     // constructor
     core(lp::lar_solver& s, params_ref const& p, reslimit&);
@@ -230,6 +233,7 @@ public:
 
     std::ostream & display_row(std::ostream& out, lp::row_strip<lp::mpq> const& row) const;
     std::ostream & display(std::ostream& out);
+    std::ostream& display_smt(std::ostream& out);
     std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
     std::ostream & print_var(lpvar j, std::ostream & out) const;
     std::ostream & print_monics(std::ostream & out) const;    
diff --git a/src/math/lp/nla_pp.cpp b/src/math/lp/nla_pp.cpp
index feb41faee..f4bfc1f8f 100644
--- a/src/math/lp/nla_pp.cpp
+++ b/src/math/lp/nla_pp.cpp
@@ -315,4 +315,122 @@ std::ostream& core::display(std::ostream& out) {
     for (auto& m : m_emons)
         print_monic(m, out);
     return out;
+}
+
+std::ostream& core::display_smt(std::ostream& out) {
+    out << "(set-option :unsat_core true)\n";
+    display_declarations_smt(out);
+    unsigned id = 0;
+    for (auto& c : lra.constraints().active())
+        display_constraint_smt(out, id++, c);
+    out << "(check-sat)\n";
+    out << "(get-unsat-core)\n";
+    out << "(reset)\n";
+    return out;
+}
+
+
+std::ostream& core::display_declarations_smt(std::ostream& out) const {
+    for (unsigned v = 0; v < lra.column_count(); ++v) {
+        if (is_monic_var(v)) {
+            out << "(define-const x" << v << " ";
+            out << (lra.var_is_int(v) ? "Int" : "Real");
+            auto const& m = m_emons[v];
+            out << " (*";
+            for (auto w : m.vars())
+                out << " x" << w;
+            out << ")";
+            out << "); " << val(v) << " = ";
+            rational p(1);
+            for (auto w : m.vars())
+                p *= val(v);
+            out << p;
+            out << "\n";
+        } 
+        else {
+            out << "(declare-const x" << v << " ";
+            out << (lra.var_is_int(v) ? "Int" : "Real");
+            out << "); " << val(v) << "\n";
+        }
+    }
+    return out;
+}
+
+std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const {
+    auto k = c.kind();
+    auto rhs = c.rhs();
+    auto lhs = c.coeffs();
+    auto sz = lhs.size();
+    rational den = denominator(rhs);
+    for (auto [coeff, v] : lhs) 
+        den = lcm(den, denominator(coeff));
+    rhs *= den;  
+
+    auto value_of = [&](lp::lpvar v) {
+        if (is_monic_var(v)) {
+            auto& m = m_emons[v];
+            rational p(1);
+            for (auto w : m.vars())
+                p *= val(w);
+            return p;
+        }
+        return val(v);
+    };
+
+    switch (k) {
+    case lp::lconstraint_kind::LE:
+        out << "(assert (! (<= ";
+        break;
+    case lp::lconstraint_kind::GE:
+        out << "(assert (! (>= ";
+        break;
+    case lp::lconstraint_kind::LT:
+        out << "(assert (! (< ";
+        break;
+    case lp::lconstraint_kind::GT:
+        out << "(assert (! (> ";
+        break;
+    case lp::lconstraint_kind::EQ:
+        out << "(assert (! (= ";
+        break;
+    default:
+        UNREACHABLE();  // unreachable
+    }
+    rational lhs_val(0);
+    if (lhs.size() > 1)
+        out << "(+";
+    for (auto [coeff, v] : lhs) {
+        auto c = coeff * den;
+        if (c == 1)
+            out << " x" << v;
+        else
+            out << " (* " << c << " x" << v << ")";
+        lhs_val += value_of(v) * c;
+    }
+    if (lhs.size() > 1)
+        out << ")";
+    out << " " << rhs << ") :named a" << id << ")); ";
+    bool evaluation = true;
+    switch (k) {
+        case lp::lconstraint_kind::LE:
+            evaluation = lhs_val <= rhs;
+            break;
+        case lp::lconstraint_kind::GE:
+            evaluation = lhs_val >= rhs;
+            break;
+        case lp::lconstraint_kind::LT:
+            evaluation = lhs_val < rhs;
+            break;
+        case lp::lconstraint_kind::GT:
+            evaluation = lhs_val > rhs;
+            break;
+        case lp::lconstraint_kind::EQ:
+            evaluation = lhs_val == rhs;
+            break;            
+        default:
+            UNREACHABLE();  // unreachable
+    }
+    out << (evaluation ? "true" : "false");
+    out << "\n";
+    return out;
 }
\ No newline at end of file