diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 647f8681c..beda1b901 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -57,17 +57,8 @@ namespace sat {
     }
 
     std::ostream& drat::pp(std::ostream& out, status st) const {
-        if (st.is_redundant())
-            out << "l";
-        else if (st.is_deleted())
+        if (st.is_deleted())
             out << "d";
-        else if (st.is_asserted())
-            out << "a";
-        else if (st.is_input())
-            out << "i";
-
-        if (!st.is_sat())
-            out << " " << m_theory[st.get_th()];
         return out;
     }
 
@@ -102,11 +93,6 @@ namespace sat {
             }
         }
 
-        if (!st.is_sat()) {
-            for (char ch : m_theory[st.get_th()])
-                buffer[len++] = ch;
-            buffer[len++] = ' ';
-        }
         for (unsigned i = 0; i < n; ++i) {
             literal lit = c[i];
             unsigned v = lit.var();
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 452b69701..7c39f5f41 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -17,39 +17,6 @@ Notes:
 
     For DIMACS input it produces DRAT proofs.
 
-    For SMT extensions are as follows:
-
-    Input assertion:
-      i <literal>* 0
-
-    Assertion (true modulo a theory):
-      a [<theory-id>] <literal>* 0
-    The if no theory id is given, the assertion is a tautology
-    modulo Tseitin converison. Theory ids track whether the
-    tautology is modulo a theory.
-    Assertions are irredundant.
-
-    Bridge from ast-node to boolean variable:
-      b <bool-var-id> <ast-node-id> 0
-
-    Definition of an expression (ast-node):
-      e <ast-node-id> <name> <ast-node-id>* 0
-
-    Redundant clause (theory lemma if theory id is given)
-      [r [<theory-id>]] <literal>* 0
-
-    Declaration of an auxiliary function:
-      f <smtlib2-function-declaration> 0
-
-    Garbage collection of a Boolean variable:
-      g <bool-var-id> 0
-
-    Available theories are:
-      - euf   The theory lemma should be a consequence of congruence closure.
-      - ba    TBD (need to also log cardinality and pb constraints)
-
-    Life times of theory lemmas is TBD. When they are used for conflict resolution
-    they are only used for the next lemma.
 
 --*/
 #pragma once
@@ -89,7 +56,6 @@ namespace sat {
         svector<std::pair<literal, clause*>> m_units;
         vector<watch>           m_watches;
         svector<lbool>          m_assignment;
-        vector<std::string>     m_theory;
         bool                    m_inconsistent = false;
         bool                    m_check_unsat = false;
         bool                    m_check_sat = false;
@@ -135,7 +101,6 @@ namespace sat {
 
         void updt_config();
 
-        void add_theory(int id, symbol const& s) { m_theory.setx(id, s.str(), std::string()); }
         void add();
         void add(literal l, bool learned);
         void add(literal l1, literal l2, status st);
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index a8a9523fd..877375246 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -37,8 +37,6 @@ namespace euf {
             !s().get_config().m_smt_proof.is_non_empty_string())
             return;
         
-        get_drat().add_theory(get_id(), symbol("euf"));
-        get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
         if (s().get_config().m_smt_proof.is_non_empty_string())
             m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out);
         get_drat().set_clause_eh(*this);
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 737148cd7..7b02509ee 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -149,8 +149,6 @@ namespace euf {
 
     void solver::add_solver(th_solver* th) {
         family_id fid = th->get_id();
-        if (use_drat())
-            s().get_drat().add_theory(fid, th->name());
         th->set_solver(m_solver);
         th->push_scopes(s().num_scopes() + s().num_user_scopes());
         m_solvers.push_back(th);