diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 30eab0b53..04a3ae4ef 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -20,9 +20,8 @@ Author:
 
 namespace arith {
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
         init_internalize();
-        flet<bool> _is_learned(m_is_redundant, learned);
         internalize_atom(e);
         literal lit = ctx.expr2literal(e);
         if (sign)
@@ -30,9 +29,8 @@ namespace arith {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
+    void solver::internalize(expr* e) {
         init_internalize();
-        flet<bool> _is_learned(m_is_redundant, redundant);
         if (m.is_bool(e))
             internalize_atom(e);
         else
@@ -247,7 +245,7 @@ namespace arith {
                     ctx.push(push_back_vector(m_idiv_terms));
                     m_idiv_terms.push_back(n);
                     app_ref mod(a.mk_mod(n1, n2), m);
-                    internalize(mod, m_is_redundant);
+                    internalize(mod);
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);
                 }
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index eb0af0c69..a658315e3 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -952,7 +952,6 @@ namespace arith {
     sat::check_result solver::check() {
         force_push();
         m_model_is_initialized = false;
-        flet<bool> _is_learned(m_is_redundant, true);
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
         SASSERT(lp().ax_is_correct());
 
@@ -1174,7 +1173,7 @@ namespace arith {
             for (auto const& c : core)
                 m_core2.push_back(~c);
             m_core2.push_back(lit);
-            add_clause(m_core2, pma);
+            add_redundant(m_core2, pma);
         }
         else {
             auto* jst = euf::th_explain::propagate(*this, core, eqs, lit, pma);
@@ -1215,7 +1214,7 @@ namespace arith {
         for (literal& c : m_core)
             c.neg();
 
-        add_clause(m_core, explain(hint_type::farkas_h));
+        add_redundant(m_core, explain(hint_type::farkas_h));
     }
 
     bool solver::is_infeasible() const {
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 3d3f1ddd7..775fecd70 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -504,8 +504,8 @@ namespace arith {
         void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         void eq_internalized(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override {}
         bool is_shared(theory_var v) const override;
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 4df4f3a50..c7517f5a4 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -20,9 +20,9 @@ Author:
 
 namespace array {
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { 
+    sat::literal solver::internalize(expr* e, bool sign, bool root) { 
         SASSERT(m.is_bool(e));
-        if (!visit_rec(m, e, sign, root, redundant)) {
+        if (!visit_rec(m, e, sign, root)) {
             TRACE("array", tout << mk_pp(e, m) << "\n";);
             return sat::null_literal;
         }
@@ -32,8 +32,8 @@ namespace array {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
-        visit_rec(m, e, false, false, redundant);
+    void solver::internalize(expr* e) {
+        visit_rec(m, e, false, false);
     }
 
     euf::theory_var solver::mk_var(euf::enode* n) {
@@ -66,7 +66,7 @@ namespace array {
         if (visited(e))
             return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
-            ctx.internalize(e, m_is_redundant);
+            ctx.internalize(e);
             euf::enode* n = expr2enode(e);
             ensure_var(n);
             return true;
diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index 5c2708842..4f100d694 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -296,8 +296,8 @@ namespace array {
         bool include_func_interp(func_decl* f) const override { return a.is_ext(f); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         euf::theory_var mk_var(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override;
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index cffd62acd..99d2a34ae 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -99,10 +99,10 @@ namespace bv {
         get_var(n);
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
         force_push();
         SASSERT(m.is_bool(e));
-        if (!visit_rec(m, e, sign, root, redundant))
+        if (!visit_rec(m, e, sign, root))
             return sat::null_literal;
         sat::literal lit = expr2literal(e);
         if (sign)
@@ -110,14 +110,14 @@ namespace bv {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
+    void solver::internalize(expr* e) {
         force_push();
-        visit_rec(m, e, false, false, redundant);
+        visit_rec(m, e, false, false);
     }
 
     bool solver::visit(expr* e) {      
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
-            ctx.internalize(e, m_is_redundant);
+            ctx.internalize(e);
             return true;
         }
         m_stack.push_back(sat::eframe(e));
@@ -246,7 +246,7 @@ namespace bv {
         for (unsigned i = 0; i < bv_size; i++) {
             expr_ref b2b(bv.mk_bit2bool(e, i), m);
             m_bits[v].push_back(sat::null_literal);
-            sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant);
+            sat::literal lit = ctx.internalize(b2b, false, false);
             TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
             if (m_bits[v].back() == sat::null_literal)
                 m_bits[v].back() = lit;
@@ -344,7 +344,7 @@ namespace bv {
             SASSERT(bits.size() == m_bits[v].size());
             unsigned i = 0;
             for (expr* bit : bits) {
-                sat::literal lit = ctx.internalize(bit, false, false, m_is_redundant);
+                sat::literal lit = ctx.internalize(bit, false, false);
                 TRACE("bv", tout << "set " << m_bits[v][i] << " == " << lit << "\n";);
                 add_clause(~lit, m_bits[v][i]);
                 add_clause(lit, ~m_bits[v][i]);
@@ -353,7 +353,7 @@ namespace bv {
             return;
         }
         for (expr* bit : bits) 
-            add_bit(v, ctx.internalize(bit, false, false, m_is_redundant));        
+            add_bit(v, ctx.internalize(bit, false, false));        
         for (expr* bit : bits)
             get_var(expr2enode(bit));
         SASSERT(get_bv_size(n) == bits.size());
@@ -371,7 +371,7 @@ namespace bv {
     sat::literal solver::mk_true() {
         if (m_true == sat::null_literal) {
             ctx.push(value_trail<sat::literal>(m_true));
-            m_true = ctx.internalize(m.mk_true(), false, true, false);
+            m_true = ctx.internalize(m.mk_true(), false, true);
             s().assign_unit(m_true);
         }
         return m_true;
@@ -493,7 +493,7 @@ namespace bv {
             m_bb.mk_sle(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le);
         else
             m_bb.mk_ule(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le);
-        literal def = ctx.internalize(le, false, false, m_is_redundant);
+        literal def = ctx.internalize(le, false, false);
         if (Negated)
             def.neg();
         add_def(def, expr2literal(n));
@@ -598,7 +598,7 @@ namespace bv {
         get_arg_bits(n, 1, arg2_bits);
         expr_ref out(m);
         fn(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), out);
-        sat::literal def = ctx.internalize(out, false, false, m_is_redundant);
+        sat::literal def = ctx.internalize(out, false, false);
         add_def(def, expr2literal(n));
     }
 
@@ -753,12 +753,11 @@ namespace bv {
             return;
         if (v1 > v2)
             std::swap(v1, v2);
-        flet<bool> _red(m_is_redundant, true);
         ++m_stats.m_ackerman;
         expr* o1 = var2expr(v1);
         expr* o2 = var2expr(v2);
         expr_ref oe = mk_var_eq(v1, v2);
-        literal oeq = ctx.internalize(oe, false, false, m_is_redundant);
+        literal oeq = ctx.internalize(oe, false, false);
         unsigned sz = m_bits[v1].size();
         TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";);
         literal_vector eqs;
@@ -772,6 +771,7 @@ namespace bv {
             eqs.push_back(~eq);
         }
         TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);
-        add_clause(eqs);
+        euf::th_proof_hint* ph = ctx.mk_smt_clause(name(), eqs.size(), eqs.data());
+        s().mk_clause(eqs, sat::status::th(true, m.get_basic_family_id(), ph));
     }
 }
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index c50f7c4e6..f103f876a 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -168,7 +168,7 @@ namespace bv {
         TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
         m_stats.m_num_diseq_static++;
         expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
-        add_unit(~ctx.internalize(eq, false, false, m_is_redundant));
+        add_unit(~ctx.internalize(eq, false, false));
     }
 
     std::ostream& solver::display(std::ostream& out, theory_var v) const {
@@ -464,7 +464,7 @@ namespace bv {
         m_lit_head = m_lit_tail;
         m_lit_tail = m_proof_literals.size();        
         proof_hint* ph = new (get_region()) proof_hint(c.m_kind, m_proof_literals, m_lit_head, m_lit_tail, a1, a2, b1, b2);
-        auto st = sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
+        auto st = sat::status::th(false, m.get_basic_family_id(), ph);
         ctx.get_drat().add(lits, st);
         m_lit_head = m_lit_tail;
         // TBD, a proper way would be to delete the lemma after use.
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index e4a44e769..dc9cd1456 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -385,8 +385,8 @@ namespace bv {
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override { return false; }
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         void eq_internalized(euf::enode* n) override;
         euf::theory_var mk_var(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode * n, sort * s) override;
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index a87f8770b..56a224d36 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -804,8 +804,8 @@ namespace dt {
     }
 
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        if (!visit_rec(m, e, sign, root, redundant)) 
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
+        if (!visit_rec(m, e, sign, root)) 
             return sat::null_literal;        
         auto lit = ctx.expr2literal(e);
         if (sign)
@@ -813,15 +813,15 @@ namespace dt {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
-        visit_rec(m, e, false, false, redundant);
+    void solver::internalize(expr* e) {
+        visit_rec(m, e, false, false);
     }
 
     bool solver::visit(expr* e) {
         if (visited(e))
             return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
-            ctx.internalize(e, m_is_redundant);
+            ctx.internalize(e);
             if (is_datatype(e))
                 mk_var(expr2enode(e));
             return true;
diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h
index 4e2524f6b..51a7679fd 100644
--- a/src/sat/smt/dt_solver.h
+++ b/src/sat/smt/dt_solver.h
@@ -154,8 +154,8 @@ namespace dt {
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         bool include_func_interp(func_decl* f) const override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         euf::theory_var mk_var(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override { return false; }
diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp
index 19b1a28de..906120314 100644
--- a/src/sat/smt/euf_ackerman.cpp
+++ b/src/sat/smt/euf_ackerman.cpp
@@ -189,7 +189,6 @@ namespace euf {
     }
 
     void ackerman::add_cc(expr* _a, expr* _b) {     
-        flet<bool> _is_redundant(ctx.m_is_redundant, true);
         app* a = to_app(_a);
         app* b = to_app(_b);
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
@@ -213,7 +212,6 @@ namespace euf {
     void ackerman::add_eq(expr* a, expr* b, expr* c) {
         if (a == c || b == c)
             return;
-        flet<bool> _is_redundant(ctx.m_is_redundant, true);
         sat::literal lits[3];
         expr_ref eq1(ctx.mk_eq(a, c), m);
         expr_ref eq2(ctx.mk_eq(b, c), m);
@@ -223,7 +221,7 @@ namespace euf {
         lits[1] = ~ctx.mk_literal(eq2);
         lits[2] = ctx.mk_literal(eq3);
         th_proof_hint* ph = ctx.mk_tc_proof_hint(lits);
-        ctx.s().mk_clause(3, lits, sat::status::th(true, m.get_basic_family_id(), ph));        
+        ctx.s().add_clause(3, lits, sat::status::th(true, m.get_basic_family_id(), ph));        
     }
 
 }
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index c0b2540ea..e2b116ea2 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -34,28 +34,28 @@ Notes:
 
 namespace euf {
 
-    void solver::internalize(expr* e, bool redundant) {
+    void solver::internalize(expr* e) {
         if (get_enode(e))
             return;
         if (si.is_bool_op(e))
-            attach_lit(si.internalize(e, redundant), e);
+            attach_lit(si.internalize(e), e);
         else if (auto* ext = expr2solver(e))
-            ext->internalize(e, redundant);
+            ext->internalize(e);
         else
-            visit_rec(m, e, false, false, redundant);
+            visit_rec(m, e, false, false);
         SASSERT(m_egraph.find(e));
     }
 
     sat::literal solver::mk_literal(expr* e) {
         expr_ref _e(e, m);
         bool is_not = m.is_not(e, e);
-        sat::literal lit = internalize(e, false, false, m_is_redundant);
+        sat::literal lit = internalize(e, false, false);
         if (is_not)
             lit.neg();
         return lit;
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
         euf::enode* n = get_enode(e);
         if (n) {
             if (m.is_bool(e)) {
@@ -67,14 +67,14 @@ namespace euf {
             return sat::null_literal;
         }
         if (si.is_bool_op(e)) {
-            sat::literal lit = attach_lit(si.internalize(e, redundant), e);
+            sat::literal lit = attach_lit(si.internalize(e), e);
             if (sign) 
                 lit.neg();
             return lit;
         }
         if (auto* ext = expr2solver(e))
-            return ext->internalize(e, sign, root, redundant);
-        if (!visit_rec(m, e, sign, root, redundant)) {
+            return ext->internalize(e, sign, root);
+        if (!visit_rec(m, e, sign, root)) {
             TRACE("euf", tout << "visit-rec\n";);          
             return sat::null_literal;
         }
@@ -89,13 +89,13 @@ namespace euf {
         th_solver* s = nullptr;        
         if (n && !si.is_bool_op(e) && (s = expr2solver(e), s && euf::null_theory_var == n->get_th_var(s->get_id()))) {
             // ensure that theory variables are attached in shared contexts. See notes (*)
-            s->internalize(e, false);
+            s->internalize(e);
             return true;
         }
         if (n)
             return true;
         if (si.is_bool_op(e)) {
-            attach_lit(si.internalize(e, m_is_redundant), e);
+            attach_lit(si.internalize(e), e);
             return true;
         }
         if (is_app(e) && to_app(e)->get_num_args() > 0) {
@@ -103,7 +103,7 @@ namespace euf {
             return false;
         }        
         if (auto* s = expr2solver(e))
-            s->internalize(e, m_is_redundant);            
+            s->internalize(e);            
         else 
             attach_node(mk_enode(e, 0, nullptr));        
         return true;
@@ -118,7 +118,7 @@ namespace euf {
             return false;
         SASSERT(!get_enode(e));
         if (auto* s = expr2solver(e)) 
-            s->internalize(e, m_is_redundant);        
+            s->internalize(e);        
         else 
             attach_node(mk_enode(e, num, m_args.data()));        
         return true;
@@ -167,8 +167,8 @@ namespace euf {
                 ph1 = mk_smt_hint(symbol("tseitin"), ~lit, lit2);
                 ph2 = mk_smt_hint(symbol("tseitin"), lit, ~lit2);
             }
-            s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph1));
-            s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id(), ph2));
+            s().mk_clause(~lit, lit2, sat::status::th(false, m.get_basic_family_id(), ph1));
+            s().mk_clause(lit, ~lit2, sat::status::th(false, m.get_basic_family_id(), ph2));
             add_aux(~lit, lit2);
             add_aux(lit, ~lit2);
             lit = lit2;
@@ -258,7 +258,7 @@ namespace euf {
             }
             pb_util pb(m);
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
-            sat::literal lit = si.internalize(at_least2, m_is_redundant);
+            sat::literal lit = si.internalize(at_least2);
             s().add_clause(lit, mk_distinct_status(lit));
         }
     }
@@ -331,7 +331,7 @@ namespace euf {
             }
             expr_ref fml = mk_or(eqs);
             sat::literal dist(si.to_bool_var(e), false);
-            sat::literal some_eq = si.internalize(fml, m_is_redundant);
+            sat::literal some_eq = si.internalize(fml);
             add_root(~dist, ~some_eq);
             add_root(dist, some_eq);
             s().add_clause(~dist, ~some_eq, mk_distinct_status(~dist, ~some_eq));
@@ -461,7 +461,7 @@ namespace euf {
     euf::enode* solver::e_internalize(expr* e) {
         euf::enode* n = m_egraph.find(e);
         if (!n) {
-            internalize(e, m_is_redundant);
+            internalize(e);
             n = m_egraph.find(e);
         }
         return n;
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 742e00cd7..a8a9523fd 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -238,12 +238,12 @@ namespace euf {
 
     sat::status solver::mk_tseitin_status(unsigned n, sat::literal const* lits) {
         th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("tseitin"), n, lits) : nullptr;
-        return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);        
+        return sat::status::th(false, m.get_basic_family_id(), ph);        
     }
 
     sat::status solver::mk_distinct_status(unsigned n, sat::literal const* lits) {
         th_proof_hint* ph = use_drat() ? mk_smt_hint(symbol("alldiff"), n, lits) : nullptr;
-        return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
+        return sat::status::th(false, m.get_basic_family_id(), ph);
     }
     
     expr* smt_proof_hint::get_hint(euf::solver& s) const {
@@ -294,7 +294,7 @@ namespace euf {
             lits.push_back(jst.lit_consequent());
         if (jst.eq_consequent().first != nullptr) 
             lits.push_back(add_lit(jst.eq_consequent()));
-        get_drat().add(lits, sat::status::th(m_is_redundant, jst.ext().get_id(), jst.get_pragma()));
+        get_drat().add(lits, sat::status::th(false, jst.ext().get_id(), jst.get_pragma()));
         for (unsigned i = s().num_vars(); i < nv; ++i)
             set_tmp_bool_var(i, nullptr);
     }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 149e3b1a2..737148cd7 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -655,14 +655,14 @@ namespace euf {
             if (si.is_bool_op(e)) 
                 lit = literal(replay.m[e], false);
             else 
-                lit = si.internalize(e, false);
+                lit = si.internalize(e);
             VERIFY(lit.var() == v);     
             if (!m_egraph.find(e) && !m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e) && !m.is_implies(e) && !m.is_xor(e)) {
                 ptr_buffer<euf::enode> args;
                 if (is_app(e))
                     for (expr* arg : *to_app(e))
                         args.push_back(e_internalize(arg));
-                internalize(e, true);
+                internalize(e);
                 if (!m_egraph.find(e))
                     mk_enode(e, args.size(), args.data());
             }
@@ -692,10 +692,10 @@ namespace euf {
             disable_relevancy(e);
             return;
         }
-        auto lit = si.internalize(e, true);
+        auto lit = si.internalize(e);
         switch (to_app(e)->get_decl_kind()) {
         case OP_NOT: {
-            auto lit2 = si.internalize(to_app(e)->get_arg(0), true);
+            auto lit2 = si.internalize(to_app(e)->get_arg(0));
             add_aux(lit, lit2);
             add_aux(~lit, ~lit2);
             break;
@@ -705,8 +705,8 @@ namespace euf {
                 disable_relevancy(e);
                 return;
             }
-            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
-            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            auto lit1 = si.internalize(to_app(e)->get_arg(0));
+            auto lit2 = si.internalize(to_app(e)->get_arg(1));
             add_aux(~lit, ~lit1, lit2);
             add_aux(~lit, lit1, ~lit2);
             add_aux(lit, lit1, lit2);
@@ -716,7 +716,7 @@ namespace euf {
         case OP_OR: {
             sat::literal_vector lits;
             for (expr* arg : *to_app(e))
-                lits.push_back(si.internalize(arg, true));
+                lits.push_back(si.internalize(arg));
             for (auto lit2 : lits)
                 add_aux(~lit2, lit);
             lits.push_back(~lit);
@@ -726,7 +726,7 @@ namespace euf {
         case OP_AND: {
             sat::literal_vector lits;
             for (expr* arg : *to_app(e))
-                lits.push_back(~si.internalize(arg, true));
+                lits.push_back(~si.internalize(arg));
             for (auto nlit2 : lits)
                 add_aux(~lit, ~nlit2);
             lits.push_back(lit);
@@ -740,9 +740,9 @@ namespace euf {
             add_aux(~lit);
             break;
         case OP_ITE: {
-            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
-            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
-            auto lit3 = si.internalize(to_app(e)->get_arg(2), true);
+            auto lit1 = si.internalize(to_app(e)->get_arg(0));
+            auto lit2 = si.internalize(to_app(e)->get_arg(1));
+            auto lit3 = si.internalize(to_app(e)->get_arg(2));
             add_aux(~lit, ~lit1, lit2);
             add_aux(~lit, lit1, lit3);
             add_aux(lit, ~lit1, ~lit2);
@@ -754,8 +754,8 @@ namespace euf {
                 disable_relevancy(e);
                 break;
             }
-            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
-            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            auto lit1 = si.internalize(to_app(e)->get_arg(0));
+            auto lit2 = si.internalize(to_app(e)->get_arg(1));
             add_aux(lit, ~lit1, lit2);
             add_aux(lit, lit1, ~lit2);
             add_aux(~lit, lit1, lit2);
@@ -767,8 +767,8 @@ namespace euf {
                 disable_relevancy(e);
                 break;
             }
-            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
-            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            auto lit1 = si.internalize(to_app(e)->get_arg(0));
+            auto lit2 = si.internalize(to_app(e)->get_arg(1));
             add_aux(~lit, ~lit1, lit2);
             add_aux(lit, lit1);
             add_aux(lit, ~lit2);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 5e12324a4..beb0809fb 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -439,8 +439,8 @@ namespace euf {
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
 
         // internalize
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool learned) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         sat::literal mk_literal(expr* e);
         void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); }
         void attach_node(euf::enode* n);
diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index 4a5795953..1de72d80b 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -95,9 +95,9 @@ namespace fpa {
         TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_expr(), m) << " := " << v << "\n";);
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
         SASSERT(m.is_bool(e));
-        if (!visit_rec(m, e, sign, root, redundant))
+        if (!visit_rec(m, e, sign, root))
             return sat::null_literal;
         sat::literal lit = expr2literal(e);
         if (sign)
@@ -105,8 +105,8 @@ namespace fpa {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
-        visit_rec(m, e, false, false, redundant);
+    void solver::internalize(expr* e) {
+        visit_rec(m, e, false, false);
     }
 
     bool solver::visited(expr* e) {
@@ -118,7 +118,7 @@ namespace fpa {
         if (visited(e))
             return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
-            ctx.internalize(e, m_is_redundant);
+            ctx.internalize(e);
             return true;
         }
         m_stack.push_back(sat::eframe(e));
diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h
index 38abb399d..1473ec463 100644
--- a/src/sat/smt/fpa_solver.h
+++ b/src/sat/smt/fpa_solver.h
@@ -59,8 +59,8 @@ namespace fpa {
         bool use_diseqs() const override { return true; }
         void new_diseq_eh(euf::th_eq const& eq) override;
 
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
 
         std::ostream& display(std::ostream& out) const override;
diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp
index eae1bbe5a..af25e7a92 100644
--- a/src/sat/smt/pb_internalize.cpp
+++ b/src/sat/smt/pb_internalize.cpp
@@ -22,12 +22,11 @@ Author:
 
 namespace pb {
 
-    void solver::internalize(expr* e, bool redundant) {
-        internalize(e, false, false, redundant);
+    void solver::internalize(expr* e) {
+        internalize(e, false, false);
     }
 
-    literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        flet<bool> _redundant(m_is_redundant, redundant);
+    literal solver::internalize(expr* e, bool sign, bool root) {
         if (m_pb.is_pb(e)) {
             sat::literal lit = internalize_pb(e, sign, root);
             if (m_ctx && !root && lit != sat::null_literal)
@@ -84,7 +83,7 @@ namespace pb {
 
     void solver::convert_pb_args(app* t, literal_vector& lits) {
         for (expr* arg : *t) {
-            lits.push_back(si.internalize(arg, m_is_redundant));
+            lits.push_back(si.internalize(arg));
             s().set_external(lits.back().var());
         }
     }
diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h
index 09c0e47e0..f6a0c049e 100644
--- a/src/sat/smt/pb_solver.h
+++ b/src/sat/smt/pb_solver.h
@@ -402,8 +402,8 @@ namespace pb {
         bool is_blocked(literal l, sat::ext_constraint_idx idx) override;
         bool check_model(sat::model const& m) const override;
 
-        literal internalize(expr* e, bool sign, bool root, bool redundant) override;
-        void internalize(expr* e, bool redundant) override;
+        literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
         euf::th_solver* clone(euf::solver& ctx) override;
 
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index ae37b7f07..26c99180b 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -53,7 +53,7 @@ namespace q {
         if (!m_flat.find(q, q_flat)) {
             if (expand(q)) {
                 for (expr* e : m_expanded) {
-                    sat::literal lit = ctx.internalize(e, l.sign(), false, false);
+                    sat::literal lit = ctx.internalize(e, l.sign(), false);
                     add_clause(~l, lit);
                 }
                 return;
@@ -62,7 +62,7 @@ namespace q {
         }
             
         if (is_ground(q_flat->get_expr())) {
-            auto lit = ctx.internalize(q_flat->get_expr(), l.sign(), false, false);
+            auto lit = ctx.internalize(q_flat->get_expr(), l.sign(), false);
             add_clause(~l, lit);
         }
         else {
@@ -163,7 +163,7 @@ namespace q {
         m_mbqi.init_search();
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
         SASSERT(is_forall(e) || is_exists(e));
         sat::bool_var v = ctx.get_si().add_bool_var(e);
         sat::literal lit = ctx.attach_lit(sat::literal(v, false), e);
diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h
index 153cdc774..d0581f852 100644
--- a/src/sat/smt/q_solver.h
+++ b/src/sat/smt/q_solver.h
@@ -95,8 +95,8 @@ namespace q {
         void collect_statistics(statistics& st) const override;
         euf::th_solver* clone(euf::solver& ctx) override;
         bool unit_propagate() override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override { internalize(e, false, false, redundant); }
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override { internalize(e, false, false); }
         euf::theory_var mk_var(euf::enode* n) override;
         void init_search() override;
         void finalize_model(model& mdl) override;
diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp
index c88138d3f..aef957034 100644
--- a/src/sat/smt/recfun_solver.cpp
+++ b/src/sat/smt/recfun_solver.cpp
@@ -232,10 +232,10 @@ namespace recfun {
         ctx.push(push_back_vector<scoped_ptr_vector<propagation_item>>(m_propagation_queue));        
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
         force_push();
         SASSERT(m.is_bool(e));
-        if (!visit_rec(m, e, sign, root, redundant)) {
+        if (!visit_rec(m, e, sign, root)) {
             TRACE("array", tout << mk_pp(e, m) << "\n";);
             return sat::null_literal;
         }
@@ -245,9 +245,9 @@ namespace recfun {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
+    void solver::internalize(expr* e) {
         force_push();
-        visit_rec(m, e, false, false, redundant);
+        visit_rec(m, e, false, false);
     }
 
     bool solver::visited(expr* e) {
@@ -259,7 +259,7 @@ namespace recfun {
         if (visited(e))
             return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
-            ctx.internalize(e, m_is_redundant);
+            ctx.internalize(e);
             return true;
         }
         m_stack.push_back(sat::eframe(e));
diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h
index 4e41a35a9..21d75623f 100644
--- a/src/sat/smt/recfun_solver.h
+++ b/src/sat/smt/recfun_solver.h
@@ -101,8 +101,8 @@ namespace recfun {
         void collect_statistics(statistics& st) const override;
         euf::th_solver* clone(euf::solver& ctx) override;
         bool unit_propagate() override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool is_shared(euf::theory_var v) const override { return true; }
diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h
index 5fbf879ae..5be20c4e0 100644
--- a/src/sat/smt/sat_internalizer.h
+++ b/src/sat/smt/sat_internalizer.h
@@ -23,7 +23,7 @@ namespace sat {
     public:
         virtual ~sat_internalizer() = default;
         virtual bool is_bool_op(expr* e) const = 0;
-        virtual literal internalize(expr* e, bool learned) = 0;
+        virtual literal internalize(expr* e) = 0;
         virtual bool_var to_bool_var(expr* e) = 0;
         virtual bool_var add_bool_var(expr* e)  = 0;
         virtual bool is_cached(app* t, literal l) const = 0;
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 81fd7e384..17d167829 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -21,9 +21,8 @@ Author:
 
 namespace euf {
 
-    bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) {
+    bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root) {
         IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n");
-        flet<bool> _is_learned(m_is_redundant, redundant);
         svector<sat::eframe>::scoped_stack _sc(m_stack);
         unsigned sz = m_stack.size();
         visit(a);
@@ -125,15 +124,11 @@ namespace euf {
             pop_core(n);        
     }
 
-    sat::status th_euf_solver::mk_status(th_proof_hint const* ps) {
-        return sat::status::th(m_is_redundant, get_id(), ps);
-    }
-
     bool th_euf_solver::add_unit(sat::literal lit, th_proof_hint const* ps) {
         if (ctx.use_drat() && !ps)
             ps = ctx.mk_smt_clause(name(), 1, &lit);
         bool was_true = is_true(lit);
-        ctx.s().add_clause(1, &lit, mk_status(ps));
+        ctx.s().add_clause(1, &lit, sat::status::th(false, get_id(), ps));
         ctx.add_root(lit);
         return !was_true;
     }
@@ -161,7 +156,7 @@ namespace euf {
         return add_clause(4, lits, ps);
     }
 
-    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps) {
+    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps, bool is_redundant) {
         if (ctx.use_drat() && !ps) 
             ps = ctx.mk_smt_clause(name(), n, lits);
                 
@@ -169,7 +164,7 @@ namespace euf {
         for (unsigned i = 0; i < n; ++i)       
             was_true |= is_true(lits[i]);
         ctx.add_root(n, lits);
-        s().add_clause(n, lits, mk_status(ps));
+        s().add_clause(n, lits, sat::status::th(is_redundant, get_id(), ps));
         return !was_true;
     }
 
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index d64b65635..a3b81a08d 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -30,9 +30,8 @@ namespace euf {
     protected:
         euf::enode_vector     m_args;
         svector<sat::eframe>  m_stack;
-        bool                  m_is_redundant{ false };
 
-        bool visit_rec(ast_manager& m, expr* e, bool sign, bool root, bool redundant);
+        bool visit_rec(ast_manager& m, expr* e, bool sign, bool root);
 
         virtual bool visit(expr* e) { return false; }
         virtual bool visited(expr* e) { return false; }
@@ -41,9 +40,9 @@ namespace euf {
     public:
         virtual ~th_internalizer() = default;
 
-        virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0;
+        virtual sat::literal internalize(expr* e, bool sign, bool root) = 0;
 
-        virtual void internalize(expr* e, bool redundant) = 0;
+        virtual void internalize(expr* e) = 0;
 
 
         /**
@@ -135,7 +134,7 @@ namespace euf {
 
         virtual bool is_beta_redex(euf::enode* p, euf::enode* n) const { return false; }
 
-        sat::status status() const { return sat::status::th(m_is_redundant, get_id()); }
+        sat::status status() const { return sat::status::th(false, get_id()); }
 
     };
 
@@ -155,8 +154,6 @@ namespace euf {
         sat::literal expr2literal(expr* e) const;
         region& get_region();
 
-
-        sat::status mk_status(th_proof_hint const* ps = nullptr);
         bool add_unit(sat::literal lit, th_proof_hint const* ps = nullptr);
         bool add_units(sat::literal_vector const& lits);
         bool add_clause(sat::literal lit, th_proof_hint const* ps = nullptr) { return add_unit(lit, ps); }
@@ -164,9 +161,11 @@ namespace euf {
         bool add_clause(sat::literal a, sat::literal b, sat::literal c, th_proof_hint const* ps = nullptr);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d, th_proof_hint const* ps = nullptr);
         bool add_clause(sat::literal_vector const& lits, th_proof_hint const* ps = nullptr) { return add_clause(lits.size(), lits.data(), ps); }
-        bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps = nullptr);
+        bool add_clause(unsigned n, sat::literal* lits, th_proof_hint const* ps, bool is_redundant = false);
         void add_equiv(sat::literal a, sat::literal b);
         void add_equiv_and(sat::literal a, sat::literal_vector const& bs);
+        bool add_redundant(sat::literal_vector const& lits, th_proof_hint const* ps) { return add_clause(lits.size(), lits.data(), ps, true); }
+        bool add_redundant(unsigned n, sat::literal* lits, th_proof_hint const* ps);
 
 
         bool is_true(sat::literal lit);
diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp
index 5c98a6fac..99e4eeeb1 100644
--- a/src/sat/smt/user_solver.cpp
+++ b/src/sat/smt/user_solver.cpp
@@ -30,7 +30,7 @@ namespace user_solver {
 
     void solver::add_expr(expr* e) {
         force_push();
-        ctx.internalize(e, false);
+        ctx.internalize(e);
         euf::enode* n = expr2enode(e);
         if (is_attached_to_var(n))
             return;
@@ -63,7 +63,7 @@ namespace user_solver {
             return;
         }
         force_push();
-        ctx.internalize(e, false);
+        ctx.internalize(e);
         m_next_split_expr = e;
         m_next_split_idx = idx;
         m_next_split_phase = phase;
@@ -162,7 +162,7 @@ namespace user_solver {
     }
 
     void solver::propagate_consequence(prop_info const& prop) {
-        sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true);
+        sat::literal lit = ctx.internalize(prop.m_conseq, false, false);
         if (s().value(lit) != l_true) {
             s().assign(lit, mk_justification(m_qhead));
             ++m_stats.m_num_propagations;
@@ -250,8 +250,8 @@ namespace user_solver {
         return result;
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        if (!visit_rec(m, e, sign, root, redundant)) {
+    sat::literal solver::internalize(expr* e, bool sign, bool root) {
+        if (!visit_rec(m, e, sign, root)) {
             TRACE("array", tout << mk_pp(e, m) << "\n";);
             return sat::null_literal;
         }
@@ -263,15 +263,15 @@ namespace user_solver {
         return lit;
     }
 
-    void solver::internalize(expr* e, bool redundant) {
-        visit_rec(m, e, false, false, redundant);
+    void solver::internalize(expr* e) {
+        visit_rec(m, e, false, false);
     }
 
     bool solver::visit(expr* e) {
         if (visited(e))
             return true;
         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
-            ctx.internalize(e, m_is_redundant);
+            ctx.internalize(e);
             return true;
         }
         m_stack.push_back(sat::eframe(e));
diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h
index 28528b9a1..cb1c6fe94 100644
--- a/src/sat/smt/user_solver.h
+++ b/src/sat/smt/user_solver.h
@@ -154,8 +154,8 @@ namespace user_solver {
         bool unit_propagate() override;
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
         void collect_statistics(statistics& st) const override;
-        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
-        void internalize(expr* e, bool redundant) override;
+        sat::literal internalize(expr* e, bool sign, bool root) override;
+        void internalize(expr* e) override;
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index c819403d7..403cee684 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -75,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
     bool                        m_euf = false;
-    bool                        m_is_redundant = false;
     bool                        m_top_level = false;
     sat::literal_vector         aig_lits;
     
@@ -133,7 +132,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     sat::status mk_status(euf::th_proof_hint* ph = nullptr) const {
-        return sat::status::th(m_is_redundant, m.get_basic_family_id(), ph);
+        return sat::status::th(false, m.get_basic_family_id(), ph);
     }
 
     bool relevancy_enabled() {
@@ -179,7 +178,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
         if (relevancy_enabled())
             ensure_euf()->add_root(n, lits);
-        m_solver.add_clause(n, lits, m_is_redundant ? mk_status(ph) : sat::status::input());
+        m_solver.add_clause(n, lits, ph ? mk_status(ph) : sat::status::input());
     }
 
     sat::bool_var add_var(bool is_ext, expr* n) {
@@ -688,7 +687,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::literal lit;
         {
             flet<bool> _top(m_top_level, false);
-            lit = euf->internalize(e, sign, root, m_is_redundant);           
+            lit = euf->internalize(e, sign, root);           
         }
         if (lit == sat::null_literal) 
             return;
@@ -711,7 +710,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             th = dynamic_cast<euf::th_solver*>(ext);
             SASSERT(th);
         }
-        auto lit = th->internalize(t, sign, root, m_is_redundant);
+        auto lit = th->internalize(t, sign, root);
         m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
         if (lit == sat::null_literal)
             return;
@@ -780,12 +779,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     };
 
-    void process(expr* n, bool is_root, bool redundant) {
+    void process(expr* n, bool is_root) {
         TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 2) 
             << " root: " << is_root 
             << " result-stack: " << m_result_stack.size() 
             << " frame-stack: " << m_frame_stack.size() << "\n";);
-        flet<bool> _is_redundant(m_is_redundant, redundant);
         scoped_stack _sc(*this, is_root);
         unsigned sz = m_frame_stack.size();
         if (visit(n, is_root, false)) 
@@ -836,14 +834,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
             << " result-stack: " << m_result_stack.size() << "\n";);
     }
 
-    sat::literal internalize(expr* n, bool redundant) override {
+    sat::literal internalize(expr* n) override {
         bool is_not = m.is_not(n, n);
         flet<bool> _top(m_top_level, false);
         unsigned sz = m_result_stack.size();
         (void)sz;
         SASSERT(n->get_ref_count() > 0);
         TRACE("goal2sat", tout << "internalize " << mk_bounded_pp(n, m, 2) << "\n";);
-        process(n, false, redundant);
+        process(n, false);
         SASSERT(m_result_stack.size() == sz + 1);
         sat::literal result = m_result_stack.back();
         TRACE("goal2sat", tout << "done internalize " << result << " " << mk_bounded_pp(n, m, 2) << "\n";);
@@ -889,7 +887,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         flet<bool> _top(m_top_level, true);
         VERIFY(m_result_stack.empty());
         TRACE("goal2sat", tout << "assert: " << mk_bounded_pp(n, m, 3) << "\n";);
-        process(n, true, m_is_redundant);
+        process(n, true);
         CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
     }