diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index dbabb1a7b..78b207f94 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -166,7 +166,24 @@ namespace euf {
         return m.mk_app(f, args);
     }
 
+    smt_proof_hint* solver::mk_smt_clause(symbol const& n, unsigned nl, literal const* lits) {
+        if (!use_drat())
+            return nullptr;
+        push(value_trail(m_lit_tail));
+        push(restore_size_trail(m_proof_literals));
 
+        for (unsigned i = 0; i < nl; ++i)
+            m_proof_literals.push_back(~lits[i]);
+            
+        m_lit_head = m_lit_tail;
+        m_eq_head = m_eq_tail;
+        m_deq_head = m_deq_tail;
+        m_lit_tail = m_proof_literals.size();
+        m_eq_tail = m_proof_eqs.size();
+        m_deq_tail = m_proof_deqs.size();
+
+        return new (get_region()) smt_proof_hint(n, m_lit_head, m_lit_tail, m_eq_head, m_eq_tail, m_deq_head, m_deq_tail);
+    }
     
     smt_proof_hint* solver::mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd, expr_pair const* deqs) {
         if (!use_drat())
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 5e38768ee..62e7abcae 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -404,6 +404,7 @@ namespace euf {
         smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, expr* a, expr* b) { expr_pair e(a, b); return mk_smt_hint(n, 1, &lit, 0, nullptr, 1, &e); }        
         smt_proof_hint* mk_smt_prop_hint(symbol const& n, literal lit, enode* a, enode* b) { return mk_smt_prop_hint(n, lit, a->get_expr(), b->get_expr()); }
         smt_proof_hint* mk_smt_hint(symbol const& n, enode* a, enode* b) { expr_pair e(a->get_expr(), b->get_expr()); return mk_smt_hint(n, 0, nullptr, 1, &e); }
+        smt_proof_hint* mk_smt_clause(symbol const& n, unsigned nl, literal const* lits);
         th_proof_hint* mk_cc_proof_hint(sat::literal_vector const& ante, app* a, app* b);
         th_proof_hint* mk_tc_proof_hint(sat::literal const* ternary_clause);
         sat::status mk_tseitin_status(sat::literal a, sat::literal b);
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index bf2e04dc5..ad280eff8 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -160,7 +160,9 @@ namespace euf {
     }
 
     bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
-        SASSERT(!ctx.use_drat() || ps); // - very far from true, and isn't a requirement
+        if (ctx.use_drat() && !ps) 
+            ps = ctx.mk_smt_clause(name(), n, lits);
+                
         bool was_true = false;
         for (unsigned i = 0; i < n; ++i)       
             was_true |= is_true(lits[i]);