diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index ff63ae2ef..7b0fd8b57 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2168,7 +2168,21 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
     return n;
 }
 
-
+pob* pred_transformer::pob_manager::find_pob(pob* parent, expr *post) {
+    pob p(parent, m_pt, 0, 0, false);
+    p.set_post(post);
+    pob *res = nullptr;
+    if (m_pobs.contains(p.post())) {
+        for (auto *f : m_pobs[p.post()]) {
+            if (f->parent() == parent) {
+                // try to find pob not already in queue
+                if (!f->is_in_queue()) return f;
+                res = f;
+            }
+        }
+    }
+    return res;
+}
 
 
 // ----------------
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index f2242f0ad..07bea0538 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -304,6 +304,7 @@ class pred_transformer {
         }
         unsigned size() const {return m_pinned.size();}
 
+        pob* find_pob(pob* parent, expr *post);
     };
 
     class pt_rule {
@@ -601,7 +602,6 @@ class pob {
     std::map<unsigned, stopwatch> m_expand_watches;
     unsigned m_blocked_lvl;
 
-    void set_post(expr *post);
 public:
     pob (pob* parent, pred_transformer& pt,
          unsigned level, unsigned depth=0, bool add_to_parent=true);
@@ -610,6 +610,7 @@ public:
 
     // TBD: move into constructor and make private
     void set_post(expr *post, app_ref_vector const &binding);
+    void set_post(expr *post);
 
     unsigned weakness() {return m_weakness;}
     void bump_weakness() {m_weakness++;}