diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 9fe7540e0..e9d989545 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -133,7 +133,7 @@ namespace arith {
         return m_arith_hint.mk(ctx);
     }
 
-    arith_proof_hint const* solver::explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
+    arith_proof_hint const* solver::explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
         arith_proof_hint* hint = nullptr;
         if (ctx.use_drat()) {
             m_coeffs.reset();
@@ -142,7 +142,7 @@ namespace arith {
                     m_coeffs.push_back(e.coeff());
             }
                 
-            m_arith_hint.set_type(ctx, hint_type::farkas_h);
+            m_arith_hint.set_type(ctx, ty);
             if (m_coeffs.size() == core.size()) {
                 unsigned i = 0;
                 for (auto lit : core)
@@ -206,6 +206,9 @@ namespace arith {
         case hint_type::implied_eq_h:
             name = "implied-eq";
             break;
+        case hint_type::nla_h:
+            name = "nla";
+            break;
         default:
             name = "unknown-arithmetic";
             break;
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index f30c29872..5784962a5 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1155,7 +1155,7 @@ namespace arith {
         case lp::lia_move::conflict:
             TRACE("arith", tout << "conflict\n";);
             // ex contains unsat core
-            set_conflict();
+            set_conflict(hint_type::cut_h);
             return l_false;
         case lp::lia_move::undef:
             TRACE("arith", tout << "lia undef\n";);
@@ -1187,15 +1187,15 @@ namespace arith {
     void solver::get_infeasibility_explanation_and_set_conflict() {
         m_explanation.clear();
         lp().get_infeasibility_explanation(m_explanation);
-        set_conflict();
+        set_conflict(hint_type::farkas_h);
     }
 
-    void solver::set_conflict() {
+    void solver::set_conflict(hint_type ty) {
         literal_vector core;
-        set_conflict_or_lemma(core, true);
+        set_conflict_or_lemma(ty, core, true);
     }
 
-    void solver::set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
+    void solver::set_conflict_or_lemma(hint_type ty, literal_vector const& core, bool is_conflict) {
         reset_evidence();
         m_core.append(core);
         for (auto ev : m_explanation)
@@ -1212,7 +1212,7 @@ namespace arith {
                 for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()));                       
             ++m_num_conflicts;
             ++m_stats.m_conflicts;
-            auto* hint = explain_conflict(m_core, m_eqs);
+            auto* hint = explain_conflict(ty, m_core, m_eqs);
             ctx.set_conflict(euf::th_explain::conflict(*this, m_core, m_eqs, hint));
         }
         else {
@@ -1221,7 +1221,7 @@ namespace arith {
             for (literal& c : m_core)
                 c.neg();
             
-            add_redundant(m_core, explain(hint_type::farkas_h));
+            add_redundant(m_core, explain(ty));
         }
     }
 
@@ -1428,7 +1428,7 @@ namespace arith {
                 lit = ctx.expr2literal(mk_bound(ineq.term(), ineq.rs(), is_lower));
             core.push_back(pos ? lit : ~lit);
         }
-        set_conflict_or_lemma(core, false);
+        set_conflict_or_lemma(hint_type::nla_h, core, false);
     }
 
     lbool solver::check_nla() {
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 4ff46ba13..e5ba06ae6 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -52,7 +52,8 @@ namespace arith {
         farkas_h,
         bound_h,
         cut_h,
-        implied_eq_h
+        implied_eq_h,
+        nla_h
     };
 
     struct arith_proof_hint : public euf::th_proof_hint {
@@ -457,8 +458,8 @@ namespace arith {
         void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs);
 
         void get_infeasibility_explanation_and_set_conflict();
-        void set_conflict();
-        void set_conflict_or_lemma(literal_vector const& core, bool is_conflict);
+        void set_conflict(hint_type ty);
+        void set_conflict_or_lemma(hint_type ty, literal_vector const& core, bool is_conflict);
         void set_evidence(lp::constraint_index idx);
         void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, euf::th_proof_hint const* pma);
 
@@ -470,7 +471,7 @@ namespace arith {
         arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
         arith_proof_hint const* explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b);
         arith_proof_hint const* explain_trichotomy(sat::literal le, sat::literal ge, sat::literal eq);
-        arith_proof_hint const* explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
+        arith_proof_hint const* explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
         void explain_assumptions(lp::explanation const& e);