diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index df945d9bb..87c9580e0 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -854,35 +854,6 @@ void pred_transformer::find_predecessors(datalog::rule const& r, ptr_vector<func
     }
 }
 
-void pred_transformer::find_predecessors(vector<std::pair<func_decl*, unsigned> >& preds) const
-{
-    preds.reset();
-    obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
-    for (; it != end; it++) {
-        datalog::rule const& r = *it->m_value;
-        unsigned tail_sz = r.get_uninterpreted_tail_size();
-        for (unsigned ti = 0; ti < tail_sz; ti++) {
-            preds.push_back(std::make_pair (r.get_tail(ti)->get_decl(), ti));
-        }
-    }
-}
-
-
-void pred_transformer::remove_predecessors(expr_ref_vector& literals)
-{
-    // remove tags
-    for (unsigned i = 0; i < literals.size(); ) {
-        expr* l = literals[i].get();
-        m.is_not(l, l);
-        if (m_tag2rule.contains(l)) {
-            literals[i] = literals.back();
-            literals.pop_back();
-        } else {
-            ++i;
-        }
-    }
-}
-
 void pred_transformer::simplify_formulas()
 {m_frames.simplify_formulas ();}
 
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 8de4a70f8..1991aa906 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -370,9 +370,7 @@ public:
                                  unsigned level, unsigned oidx, bool must,
                                  const ptr_vector<app> **aux);
 
-    void remove_predecessors(expr_ref_vector& literals);
     void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
-    void find_predecessors(vector<std::pair<func_decl*, unsigned> >& predicates) const;
     datalog::rule const* find_rule(model &mev, bool& is_concrete,
                                    vector<bool>& reach_pred_used,
                                    unsigned& num_reuse_reach);