diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 5c945d168..6c1f068b5 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1059,7 +1059,6 @@ extern "C" {
             case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO;
             case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO;
             case OP_SPECIAL_RELATION_TC : return Z3_OP_SPECIAL_RELATION_TC;
-            case OP_SPECIAL_RELATION_TRC : return Z3_OP_SPECIAL_RELATION_TRC;
             default: UNREACHABLE();
             }
         }
diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp
index 2bb40a5e1..3b4872435 100644
--- a/src/api/api_special_relations.cpp
+++ b/src/api/api_special_relations.cpp
@@ -62,5 +62,4 @@ extern "C" {
 }
 
     MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC);
-    MK_DECL(Z3_mk_transitive_reflexive_closure, OP_SPECIAL_RELATION_TRC);
 };
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index f4db07cfc..0d9f548ef 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3671,17 +3671,6 @@ extern "C" {
      */
     Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
 
-    /**
-       \brief create transitive reflexive closure of binary relation.
-
-       \pre f is a binary relation, such that the two arguments have the same sorts.
-
-       The resulting relation f* represents the transitive-reflexive closure of f.
-
-       def_API('Z3_mk_transitive_reflexive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL)))
-     */
-    Z3_func_decl Z3_API Z3_mk_transitive_reflexive_closure(Z3_context c, Z3_func_decl f);
-
     /*@}*/
 
     /** @name Quantifiers */
diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp
index 2b280b28a..5dc5f32fe 100644
--- a/src/ast/special_relations_decl_plugin.cpp
+++ b/src/ast/special_relations_decl_plugin.cpp
@@ -26,8 +26,7 @@ special_relations_decl_plugin::special_relations_decl_plugin():
     m_po("partial-order"),
     m_plo("piecewise-linear-order"),
     m_to("tree-order"),
-    m_tc("transitive-closure"),
-    m_trc("transitive-reflexive-closure")
+    m_tc("transitive-closure")
 {}
     
 func_decl * special_relations_decl_plugin::mk_func_decl(
@@ -56,7 +55,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
     case OP_SPECIAL_RELATION_PLO: name = m_plo; break;
     case OP_SPECIAL_RELATION_TO: name = m_to; break;
     case OP_SPECIAL_RELATION_TC: name = m_tc; break;
-    case OP_SPECIAL_RELATION_TRC: name = m_trc; break;
     }
     return m_manager->mk_func_decl(name, arity, domain, range, info);
 }
@@ -68,7 +66,6 @@ void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_name
         op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
         op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
         op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC));
-        op_names.push_back(builtin_name(m_trc.bare_str(), OP_SPECIAL_RELATION_TRC));
     }
 }
 
@@ -79,7 +76,6 @@ sr_property special_relations_util::get_property(func_decl* f) const {
     case OP_SPECIAL_RELATION_PLO: return sr_plo;
     case OP_SPECIAL_RELATION_TO: return sr_to;
     case OP_SPECIAL_RELATION_TC: return sr_tc;
-    case OP_SPECIAL_RELATION_TRC: return sr_trc;
     default:
         UNREACHABLE();
         return sr_po;
diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h
index f7a3b963d..339fdc82e 100644
--- a/src/ast/special_relations_decl_plugin.h
+++ b/src/ast/special_relations_decl_plugin.h
@@ -29,7 +29,6 @@ enum special_relations_op_kind {
     OP_SPECIAL_RELATION_PLO,
     OP_SPECIAL_RELATION_TO,
     OP_SPECIAL_RELATION_TC,
-    OP_SPECIAL_RELATION_TRC,
     LAST_SPECIAL_RELATIONS_OP
 };
 
@@ -39,7 +38,6 @@ class special_relations_decl_plugin : public decl_plugin {
     symbol m_plo;
     symbol m_to;
     symbol m_tc;
-    symbol m_trc;
 public:
     special_relations_decl_plugin();
 
@@ -70,7 +68,6 @@ enum sr_property {
     sr_plo           = 0x01 | 0x02 | 0x04 | 0x08 | 0x10,  // piecewise linear order
     sr_lo            = 0x01 | 0x02 | 0x04 | 0x20,         // linear order
     sr_tc            = 0x40,                              // transitive closure of relation
-    sr_trc           = 0x42                               // transitive reflexive closure of relation
 };
 
 class special_relations_util {
@@ -93,14 +90,12 @@ public:
     func_decl* mk_plo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PLO); }
     func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); }
     func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); }
-    func_decl* mk_trc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TRC); }
 
     bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); }
     bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); }
     bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); }
     bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); }
     bool is_tc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TC); }
-    bool is_trc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TRC); }
     
     app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO,  arg1, arg2); }
     app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO,  arg1, arg2); }
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index e6234e76a..1dce9832d 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -1,4 +1,19 @@
-/**
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    theory_array_bapa.cpp
+
+Abstract:
+
+   Saturation procedure for BAPA predicates.
+   Assume there is a predicate
+
+           Size(S, n)   for S : Array(T, Bool) and n : Int
+
+   The predicate is true if S is a set of size n.
+
 
                  Size(S, n), Size(T, m)      
           S, T are intersecting. n != m or S != T
@@ -54,6 +69,12 @@ Finite domains:
 
     Model construction for infinite domains when all Size(S, m) are negative for S.
 
+Author:
+
+    Nikolaj Bjorner 2019-04-13
+
+Revision History:
+
  */
 
 #include "ast/ast_util.h"
@@ -470,8 +491,12 @@ namespace smt {
     };
 
     theory_array_bapa::theory_array_bapa(theory_array_full& th) { m_imp = alloc(imp, th);  }
+
     theory_array_bapa::~theory_array_bapa() { dealloc(m_imp); }
+
     void theory_array_bapa::internalize_size(app* term) { m_imp->internalize_size(term); }
+
     final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); }
+
     void theory_array_bapa::init_model() { m_imp->init_model(); }
 }
diff --git a/src/smt/theory_array_bapa.h b/src/smt/theory_array_bapa.h
index b3e91ca2c..e99843cdd 100644
--- a/src/smt/theory_array_bapa.h
+++ b/src/smt/theory_array_bapa.h
@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2006 Microsoft Corporation
+Copyright (c) 2019 Microsoft Corporation
 
 Module Name:
 
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index e385034b8..52708699a 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -322,9 +322,6 @@ namespace smt {
                 // we need reachability in the R graph not R* graph
                 theory_var r1 = get_representative(a.v1());
                 theory_var r2 = get_representative(a.v2());
-                if (r.m_property == sr_trc && r1 == r2) {
-                    continue;
-                }
                 if (r_graph.can_reach(r1, r2)) {
                     TRACE("special_relations", 
                           tout << a.v1() << ": " << mk_pp(arg1, m) << " -> " 
@@ -397,13 +394,6 @@ namespace smt {
         return final_check_po(r);
     }
 
-    lbool theory_special_relations::final_check_trc(relation& r) {
-        //
-        // reflexivity is enforced from propagation.
-        // enforce transitivity.
-        //
-        return final_check_tc(r);
-    }
 
     lbool theory_special_relations::final_check_to(relation& r) {
         uint_set visited, target;
@@ -510,9 +500,6 @@ namespace smt {
         case sr_tc:
             res = final_check_tc(r);
             break;
-        case sr_trc:
-            res = final_check_trc(r);
-            break;
         default:
             UNREACHABLE();
             res = l_undef;
@@ -525,7 +512,6 @@ namespace smt {
     bool theory_special_relations::extract_equalities(relation& r) {
         switch (r.m_property) {
         case sr_tc:
-        case sr_trc:
             return false;
         default:
             break;
@@ -593,30 +579,6 @@ namespace smt {
         return res;
     }
 
-    /**
-       \brief ensure that reflexivity is enforce for Transitive Reflexive closures 
-          !TRC(R)xy => x != y
-     */
-    lbool theory_special_relations::propagate_trc(atom& a) {
-        lbool res = l_true;
-        if (a.phase()) {
-            VERIFY(a.enable());
-            relation& r = a.get_relation();
-            r.m_uf.merge(a.v1(), a.v2());
-        }
-        else {
-            literal lit(a.var(), true);
-            context& ctx = get_context();
-            expr* arg1 = get_expr(a.v1());
-            expr* arg2 = get_expr(a.v2());
-            literal consequent = ~mk_eq(arg1, arg2, false);
-            justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), 1, &lit, consequent));
-            ctx.assign(consequent, j);
-            res = l_false;
-        }
-        return res;
-    }
-
     lbool theory_special_relations::propagate_tc(atom& a) {
         if (a.phase()) {
             VERIFY(a.enable());
@@ -670,9 +632,6 @@ namespace smt {
                 res = propagate_po(a);
                 break;
             case sr_tc:
-                res = propagate_trc(a);
-                break;
-            case sr_trc:
                 res = propagate_tc(a);
                 break;
             default:
@@ -1165,9 +1124,6 @@ namespace smt {
             case sr_tc:
                 init_model_po(*kv.m_value, m, true);                
                 break;
-            case sr_trc:
-                init_model_po(*kv.m_value, m, true);                
-                break;
             default:
                 // other 28 combinations of 0x1F
                 NOT_IMPLEMENTED_YET();
diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h
index ae134a366..8bf966009 100644
--- a/src/smt/theory_special_relations.h
+++ b/src/smt/theory_special_relations.h
@@ -144,7 +144,6 @@ namespace smt {
         lbool final_check_plo(relation& r);
         lbool final_check_to(relation& r);
         lbool final_check_tc(relation& r);
-        lbool final_check_trc(relation& r);
         lbool propagate(relation& r);
         lbool enable(atom& a);
         bool  extract_equalities(relation& r);
@@ -153,7 +152,6 @@ namespace smt {
         lbool  propagate_plo(atom& a);
         lbool  propagate_po(atom& a); 
         lbool  propagate_tc(atom& a); 
-        lbool  propagate_trc(atom& a); 
         theory_var mk_var(expr* e);
         void count_children(graph const& g, unsigned_vector& num_children);
         void ensure_strict(graph& g);