diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index c1f0912c0..2c7d3d5cd 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -18,7 +18,6 @@ Revision History:
 --*/
 
 #include "dl_mk_array_blast.h"
-#include "expr_safe_replace.h"
 
 
 namespace datalog {
@@ -31,7 +30,9 @@ namespace datalog {
         a(m),
         rm(ctx.get_rule_manager()),
         m_rewriter(m, m_params),
-        m_simplifier(ctx) {
+        m_simplifier(ctx),
+        m_sub(m),
+        m_next_var(0) {
         m_params.set_bool("expand_select_store",true);
         m_rewriter.updt_params(m_params);
     }
@@ -50,14 +51,63 @@ namespace datalog {
         }
         return false;
     }
+
+    expr* mk_array_blast::get_select(expr* e) const {
+        while (a.is_select(e)) {
+            e = to_app(e)->get_arg(0);
+        }
+        return e;
+    }
+
+    void mk_array_blast::get_select_args(expr* e, ptr_vector<expr>& args) const {
+        while (a.is_select(e)) {
+            app* ap = to_app(e);
+            for (unsigned i = 1; i < ap->get_num_args(); ++i) {
+                args.push_back(ap->get_arg(i));
+            }
+            e = ap->get_arg(0);
+        }
+    }
+     
+    bool mk_array_blast::insert_def(rule const& r, app* e, var* v) {
+        //
+        // For the Ackermann reduction we would like the arrays 
+        // to be variables, so that variables can be 
+        // assumed to represent difference (alias) 
+        // classes. Ehm., Soundness of this approach depends on 
+        // if the arrays are finite domains...
+        // 
+
+        if (!is_var(get_select(e))) {
+            return false;
+        }
+        if (v) {
+            m_sub.insert(e, v);
+            m_defs.insert(e, to_var(v));
+        }
+        else {
+            if (m_next_var == 0) {
+                ptr_vector<sort> vars;
+                r.get_vars(vars);
+                m_next_var = vars.size() + 1;
+            }
+            v = m.mk_var(m_next_var, m.get_sort(e));
+            m_sub.insert(e, v);
+            m_defs.insert(e, v);
+            ++m_next_var;
+        }
+        return true;
+    }
     
-    bool mk_array_blast::ackermanize(expr_ref& body, expr_ref& head) {
+    bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
         expr_ref_vector conjs(m);
         flatten_and(body, conjs);
-        defs_t defs;
-        expr_safe_replace sub(m);
+        m_defs.reset();
+        m_sub.reset();
+        m_next_var = 0;
         ptr_vector<expr> todo;
         todo.push_back(head);
+        unsigned next_var = 0;
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* e = conjs[i].get();
             expr* x, *y;
@@ -66,22 +116,17 @@ namespace datalog {
                     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))) {
+                    if (!insert_def(r, to_app(x), to_var(y))) {
                         return false;
                     }
-                    sub.insert(x, y);
-                    defs.insert(to_app(x), to_var(y));
                 }
             }
+            if (a.is_select(e) && !insert_def(r, to_app(e), 0)) {
+                return false;
+            }
             todo.push_back(e);
         }
-        // now check that all occurrences of select have been covered.
+        // now make sure to cover all occurrences.
         ast_mark mark;
         while (!todo.empty()) {
             expr* e = todo.back();
@@ -97,22 +142,28 @@ namespace datalog {
                 return false;
             }
             app* ap = to_app(e);
-            if (a.is_select(e) && !defs.contains(ap)) {
-                return false;
+            if (a.is_select(ap) && !m_defs.contains(ap)) {
+                if (!insert_def(r, ap, 0)) {
+                    return false;
+                }
+            }
+            if (a.is_select(e)) {
+                get_select_args(e, todo);
+                continue;
             }
             for (unsigned i = 0; i < ap->get_num_args(); ++i) {
                 todo.push_back(ap->get_arg(i));
             }
         }
-        sub(body);
-        sub(head);
+        m_sub(body);
+        m_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();
+        defs_t::iterator it1 = m_defs.begin(), end = m_defs.end();
         for (; it1 != end; ++it1) {
             app* a1 = it1->m_key;
             var* v1 = it1->m_value;
@@ -121,12 +172,15 @@ namespace datalog {
             for (; it2 != end; ++it2) {
                 app* a2 = it2->m_key;
                 var* v2 = it2->m_value;
-                if (a1->get_arg(0) != a2->get_arg(0)) {
+                if (get_select(a1) != get_select(a2)) {
                     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)));
+                ptr_vector<expr> args1, args2;
+                get_select_args(a1, args1);
+                get_select_args(a2, args2);
+                for (unsigned j = 0; j < args1.size(); ++j) {
+                    eqs.push_back(m.mk_eq(args1[j], args2[j]));
                 }
                 conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
             }
@@ -179,15 +233,14 @@ namespace datalog {
             }
         }
         
-        expr_ref fml1(m), fml2(m), body(m), head(m);
-        r.to_formula(fml1);
+        expr_ref fml2(m), body(m), head(m);
         body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
         head = r.get_head();
         sub(body);
         m_rewriter(body);
         sub(head);
         m_rewriter(head);
-        change = ackermanize(body, head) || change;
+        change = ackermanize(r, body, head) || change;
         if (!inserted && !change) {
             rules.add_rule(&r);
             return false;
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index 21f2a0bf7..f4b685b7a 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -25,6 +25,7 @@ Revision History:
 #include"dl_mk_interp_tail_simplifier.h"
 #include "equiv_proof_converter.h"
 #include "array_decl_plugin.h"
+#include "expr_safe_replace.h"
 
 namespace datalog {
 
@@ -32,6 +33,8 @@ namespace datalog {
        \brief Blast occurrences of arrays in rules
     */
     class mk_array_blast : public rule_transformer::plugin {
+        typedef obj_map<app, var*> defs_t;
+
         context&        m_ctx;
         ast_manager&    m;
         array_util      a;
@@ -40,13 +43,21 @@ namespace datalog {
         th_rewriter     m_rewriter;
         mk_interp_tail_simplifier m_simplifier;
 
-        typedef obj_map<app, var*> defs_t;
+        defs_t            m_defs;
+        expr_safe_replace m_sub;
+        unsigned          m_next_var;
 
         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);
+        bool ackermanize(rule const& r, expr_ref& body, expr_ref& head);
+
+        expr* get_select(expr* e) const;
+
+        void get_select_args(expr* e, ptr_vector<expr>& args) const;
+
+        bool insert_def(rule const& r, app* e, var* v);
 
     public:
         /**
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 4454e2fbf..151cc4049 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -765,6 +765,7 @@ namespace pdr {
         ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
         model_ref mdl;
         pt().get_solver().set_model(&mdl);
+        TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";);
         VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
         datalog::rule const& rl2 = pt().find_rule(*mdl);
         SASSERT(is_ini(rl2));
@@ -958,12 +959,14 @@ namespace pdr {
      */
     void model_search::update_models() {
         obj_map<expr, model*> models;
+        obj_map<expr, datalog::rule const*> rules;
         ptr_vector<model_node> todo;
         todo.push_back(m_root);
         while (!todo.empty()) {
             model_node* n = todo.back();
             if (n->get_model_ptr()) {
                 models.insert(n->state(), n->get_model_ptr());
+                rules.insert(n->state(), n->get_rule());
             }
             todo.pop_back();
             todo.append(n->children().size(), n->children().c_ptr());
@@ -973,9 +976,13 @@ namespace pdr {
         while (!todo.empty()) {
             model_node* n = todo.back();
             model* md = 0;
+            ast_manager& m = n->pt().get_manager();
             if (!n->get_model_ptr() && models.find(n->state(), md)) {
+                TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
                 model_ref mr(md);
                 n->set_model(mr);
+                datalog::rule const* rule = rules.find(n->state());
+                n->set_rule(rule);
             }
             todo.pop_back();
             todo.append(n->children().size(), n->children().c_ptr());
@@ -1037,10 +1044,6 @@ namespace pdr {
             }
             first = false;
             predicates.pop_back();
-            for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) {
-                subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
-                predicates.push_back(tmp);
-            }
             for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
                 subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
                 dctx.get_rewriter()(tmp);
@@ -1051,9 +1054,22 @@ namespace pdr {
             for (unsigned i = 0; i < constraints.size(); ++i) {
                 max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
             }
+            if (n->children().empty()) {
+                // nodes whose states are repeated 
+                // in the search tree do not have children.
+                continue;
+            }
+                  
+            SASSERT(n->children().size() == rule->get_uninterpreted_tail_size());
+
+            for (unsigned i = 0; i < rule->get_uninterpreted_tail_size(); ++i) {
+                subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
+                predicates.push_back(tmp);
+            }
             for (unsigned i = 0; i < predicates.size(); ++i) {
                 max_var = std::max(vc.get_max_var(predicates[i].get()), max_var);
             }
+
             children.append(n->children());
         }            
         return pm.mk_and(constraints);
@@ -1230,6 +1246,7 @@ namespace pdr {
           m_expanded_lvl(0),
           m_cancel(false)
     {
+        enable_trace("pdr");
     }
 
     context::~context() {