diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index b6d9f810d..07dc1a372 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -126,7 +126,15 @@ void pob::get_skolems(app_ref_vector &v) {
     }
 }
 
-
+    std::ostream &pob::display(std::ostream &out, bool full) const {
+        out << pt().head()->get_name ()
+            << " level: " << level()
+            << " depth: " << depth()
+            << " post_id: " << post()->get_id()
+            << (is_in_queue() ? " in_queue" : "");
+        if (full) out << "\n" << m_post;
+        return out;
+    }
 
 // ----------------
 // pob_queue
@@ -2174,9 +2182,7 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
     p.set_post(post, b);
 
     if (m_pobs.contains(p.post())) {
-        auto &buf = m_pobs[p.post()];
-        for (unsigned i = 0, sz = buf.size(); i < sz; ++i) {
-            pob *f = buf.get(i);
+        for (auto *f : m_pobs[p.post()]) {
             if (f->parent() == parent && !f->is_in_queue()) {
                 f->inherit(p);
                 return f;
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 93c2337e6..36f898ed1 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -693,6 +693,7 @@ public:
         if (m_ref_count == 0) {dealloc(this);}
     }
 
+    std::ostream &display(std::ostream &out, bool full = false) const;
     class on_expand_event
     {
         pob &m_p;
@@ -702,6 +703,9 @@ public:
     };
 };
 
+inline std::ostream &operator<<(std::ostream &out, pob const &p) {
+    return p.display(out);
+}
 
 struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
     bool operator() (const pob *pn1, const pob *pn2) const;