diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index 880f196a2..b22fdf7ef 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -49,6 +49,94 @@ namespace datalog {
         }
         return false;
     }
+    
+    bool mk_array_blast::ackermanize(expr_ref& body, expr_ref& head) {
+        expr_ref_vector conjs(m);
+        flatten_and(body, conjs);
+        defs_t defs;
+        expr_safe_replace sub(m);
+        ptr_vector<expr> todo;
+        todo.push_back(head);
+        for (unsigned i = 0; i < conjs.size(); ++i) {
+            expr* e = conjs[i].get();
+            expr* x, *y;
+            if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) {
+                if (a.is_select(y)) {
+                    std::swap(x,y);
+                }
+                if (a.is_select(x) && is_var(y)) {
+                    //
+                    // For the Ackermann reduction we would like the arrays 
+                    // to be variables, so that variables can be 
+                    // assumed to represent difference (alias) 
+                    // classes.
+                    // 
+                    if (!is_var(to_app(x)->get_arg(0))) {
+                        return false;
+                    }
+                    sub.insert(x, y);
+                    defs.insert(to_app(x), to_var(y));
+                }
+            }
+            todo.push_back(e);
+        }
+        // now check that all occurrences of select have been covered.
+        ast_mark mark;
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (mark.is_marked(e)) {
+                continue;
+            }
+            mark.mark(e, true);
+            if (is_var(e)) {
+                continue;
+            }
+            if (!is_app(e)) {
+                return false;
+            }
+            app* ap = to_app(e);
+            if (a.is_select(e) && !defs.contains(ap)) {
+                return false;
+            }
+            for (unsigned i = 0; i < ap->get_num_args(); ++i) {
+                todo.push_back(ap->get_arg(i));
+            }
+        }
+        sub(body);
+        sub(head);
+        conjs.reset();
+
+        // perform the Ackermann reduction by creating implications
+        // i1 = i2 => val1 = val2 for each equality pair:
+        // (= val1 (select a_i i1))
+        // (= val2 (select a_i i2))
+        defs_t::iterator it1 = defs.begin(), end = defs.end();
+        for (; it1 != end; ++it1) {
+            app* a1 = it1->m_key;
+            var* v1 = it1->m_value;
+            defs_t::iterator it2 = it1;
+            ++it2;
+            for (; it2 != end; ++it2) {
+                app* a2 = it2->m_key;
+                var* v2 = it2->m_value;
+                if (a1->get_arg(0) != a2->get_arg(0)) {
+                    continue;
+                }
+                expr_ref_vector eqs(m);
+                for (unsigned j = 1; j < a1->get_num_args(); ++j) {
+                    eqs.push_back(m.mk_eq(a1->get_arg(j), a2->get_arg(j)));
+                }
+                conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
+            }
+        }
+        if (!conjs.empty()) {
+            conjs.push_back(body);
+            body = m.mk_and(conjs.size(), conjs.c_ptr());
+        }
+        m_rewriter(body);   
+        return true;
+    }
 
     bool mk_array_blast::blast(rule& r, rule_set& rules) {
         unsigned utsz = r.get_uninterpreted_tail_size();
@@ -92,10 +180,6 @@ namespace datalog {
                 new_conjs.push_back(tmp);
             }
         }
-        if (!inserted && !change) {
-            rules.add_rule(&r);
-            return false;
-        }
         
         rule_ref_vector new_rules(rm);
         expr_ref fml1(m), fml2(m), body(m), head(m);
@@ -106,11 +190,17 @@ namespace datalog {
         m_rewriter(body);
         sub(head);
         m_rewriter(head);
+        change = ackermanize(body, head) || change;
+        if (!inserted && !change) {
+            rules.add_rule(&r);
+            return false;
+        }
+
         fml2 = m.mk_implies(body, head);
         rm.mk_rule(fml2, new_rules, r.name());
         SASSERT(new_rules.size() == 1);
 
-        TRACE("dl", tout << "new body " << mk_pp(fml2, m) << "\n";);
+        TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
         
         rules.add_rule(new_rules[0].get());
         if (m_pc) {
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index 858b9c778..1618e4fa8 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -39,10 +39,14 @@ namespace datalog {
         th_rewriter     m_rewriter;
         equiv_proof_converter* m_pc;
 
+        typedef obj_map<app, var*> defs_t;
+
         bool blast(rule& r, rule_set& new_rules);
 
         bool is_store_def(expr* e, expr*& x, expr*& y);
 
+        bool ackermanize(expr_ref& body, expr_ref& head);
+
     public:
         /**
            \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 574d44fb5..47655ac7b 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -52,6 +52,20 @@ namespace pdr {
     static bool is_infty_level(unsigned lvl) { return lvl == infty_level; }
 
     static unsigned next_level(unsigned lvl) { return is_infty_level(lvl)?lvl:(lvl+1); }
+
+    struct pp_level {
+        unsigned m_level;
+        pp_level(unsigned l): m_level(l) {}        
+    };
+
+    static std::ostream& operator<<(std::ostream& out, pp_level const& p) {
+        if (is_infty_level(p.m_level)) {
+            return out << "oo";
+        }
+        else {
+            return out << p.m_level;
+        }
+    }
     
     // ----------------
     // pred_tansformer
@@ -263,7 +277,7 @@ namespace pdr {
             else if (is_invariant(tgt_level, curr, false, assumes_level)) {
                 
                 add_property(curr, assumes_level?tgt_level:infty_level);
-                TRACE("pdr", tout << "is invariant: "<< tgt_level << " " << mk_pp(curr, m) << "\n";);              
+                TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);              
                 src[i] = src.back();
                 src.pop_back();
                 ++m_stats.m_num_propagations;
@@ -273,14 +287,7 @@ namespace pdr {
                 ++i;
             }
         }        
-        IF_VERBOSE(2, verbose_stream() << "propagate: ";
-                   if (is_infty_level(src_level)) {
-                       verbose_stream() << "infty"; 
-                   }
-                   else {
-                       verbose_stream() << src_level;
-                   }
-                   verbose_stream() << "\n";
+        IF_VERBOSE(3, verbose_stream() << "propagate: " << pp_level(src_level) << "\n";
                    for (unsigned i = 0; i < src.size(); ++i) {
                        verbose_stream() << mk_pp(src[i].get(), m) << "\n";   
                    });
@@ -304,14 +311,14 @@ namespace pdr {
         ensure_level(lvl);        
         unsigned old_level;
         if (!m_prop2level.find(lemma, old_level) || old_level < lvl) {
-            TRACE("pdr", tout << "property1: " << lvl << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
+            TRACE("pdr", tout << "property1: " << pp_level(lvl) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
             m_levels[lvl].push_back(lemma);
             m_prop2level.insert(lemma, lvl);
             m_solver.add_level_formula(lemma, lvl);
             return true;
         }
         else {
-            TRACE("pdr", tout << "old-level: " << old_level << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
+            TRACE("pdr", tout << "old-level: " << pp_level(old_level) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
             return false;
         }
     }
@@ -337,7 +344,7 @@ namespace pdr {
         for (unsigned i = 0; i < lemmas.size(); ++i) {
             expr* lemma_i = lemmas[i].get();
             if (add_property1(lemma_i, lvl)) {
-                IF_VERBOSE(2, verbose_stream() << lvl << " " << mk_pp(lemma_i, m) << "\n";);
+                IF_VERBOSE(2, verbose_stream() << pp_level(lvl) << " " << mk_pp(lemma_i, m) << "\n";);
                 for (unsigned j = 0; j < m_use.size(); ++j) {
                     m_use[j]->add_child_property(*this, lemma_i, next_level(lvl));
                 }
@@ -1914,7 +1921,7 @@ namespace pdr {
             model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1);
             ++m_stats.m_num_nodes;
             m_search.add_leaf(*child); 
-            IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+            IF_VERBOSE(3, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
             m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
         }
         check_pre_closed(n);