diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index f18e6a78e..78a1caf68 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -67,8 +67,13 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
         buffer << s << k;
         return symbol(buffer.str().c_str());            
     }
-    
-    buffer << mk_smt2_quoted_symbol(s);
+
+    if (is_smt2_quoted_symbol(s)) {
+        buffer << mk_smt2_quoted_symbol(s);
+    }
+    else {
+        buffer << s;
+    }
     if (k > 0) {
         buffer << k;
     }
diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp
index f6755bb4f..5999b751c 100644
--- a/src/muz_qe/dl_mk_extract_quantifiers.cpp
+++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp
@@ -38,12 +38,43 @@ namespace datalog {
         m_refs.reset();
     }
 
+    app_ref mk_extract_quantifiers::ensure_app(expr* e) {
+        if (is_app(e)) {
+            return app_ref(to_app(e), m);
+        }
+        else {
+            return app_ref(m.mk_eq(e, m.mk_true()), m);
+        }
+    }
+
+    void mk_extract_quantifiers::ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail) {
+        SASSERT(is_app(e));
+        SASSERT(to_app(e)->get_decl()->get_family_id() == null_family_id);
+        app* a = to_app(e);
+        expr_ref_vector args(m);        
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            expr* arg = a->get_arg(i);
+            if (is_var(arg) || m.is_value(arg)) {
+                args.push_back(arg);
+            }
+            else {
+                expr_ref new_var(m);
+                new_var = m.mk_var(++max_var, m.get_sort(arg));
+                args.push_back(new_var);
+                tail.push_back(m.mk_eq(new_var, arg));
+            }
+        }
+        tail.push_back(m.mk_app(a->get_decl(), args.size(), args.c_ptr()));
+    }
+
 
     void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) {
-        expr_ref_vector tail(m);
+        app_ref_vector tail(m);
         quantifier_ref_vector quantifiers(m);
         unsigned utsz = r.get_uninterpreted_tail_size();
         unsigned tsz = r.get_tail_size();
+        var_counter vc(true);
+        unsigned max_var = vc.get_max_var(r);
         for (unsigned i = 0; i < utsz; ++i) {
             tail.push_back(r.get_tail(i));
             if (r.is_neg_tail(i)) {
@@ -51,21 +82,37 @@ namespace datalog {
                 return;
             }
         }
+        var_subst vs(m, true);
         for (unsigned i = utsz; i < tsz; ++i) {
             app* t = r.get_tail(i);
             expr_ref_vector conjs(m);
             datalog::flatten_and(t, conjs);
-            quantifier_ref qe(m);
+            expr_ref qe(m);
             quantifier* q = 0;
             for (unsigned j = 0; j < conjs.size(); ++j) {
                 expr* e = conjs[j].get();
                 if (rule_manager::is_forall(m, e, q)) {
                     quantifiers.push_back(q);
-                    qe = m.mk_exists(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), q->get_expr());
-                    tail.push_back(qe);
+                    expr_ref_vector sub(m);
+                    ptr_vector<sort> fv;
+                    unsigned num_decls = q->get_num_decls();
+                    get_free_vars(q, fv);
+                    for (unsigned k = 0; k < fv.size(); ++k) {
+                        unsigned idx = fv.size()-k-1;
+                        if (!fv[idx]) {
+                            fv[idx] = m.mk_bool_sort();
+                        }
+                        sub.push_back(m.mk_var(idx, fv[idx]));
+                    }
+                    for (unsigned k = 0; k < num_decls; ++k) {
+                        sub.push_back(m.mk_var(num_decls+max_var-k, q->get_decl_sort(k)));
+                    }
+                    max_var += num_decls;                    
+                    vs(q->get_expr(), sub.size(), sub.c_ptr(), qe);
+                    ensure_predicate(qe, max_var, tail);
                 }
                 else {
-                    tail.push_back(e);
+                    tail.push_back(ensure_app(e));
                 }
             }
         }
@@ -73,16 +120,16 @@ namespace datalog {
             new_rules.add_rule(&r);
         }
         else {
-            expr_ref fml(m);
-            rule_ref_vector rules(rm);
-            fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head());
-            rm.mk_rule(fml, rules, r.name());
+            rule_ref new_rule(rm);
+            std::cout << mk_pp(r.get_head(), m) << " :- \n";
+            for (unsigned i = 0; i < tail.size(); ++i) {
+                std::cout << "  " << mk_pp(tail[i].get(), m) << "\n";
+            }
+            new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name(), false);
             quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers);
             m_refs.push_back(qs);
-            for (unsigned i = 0; i < rules.size(); ++i) {
-                m_quantifiers.insert(rules[i].get(), qs);
-                new_rules.add_rule(rules[i].get());
-            }
+            new_rules.add_rule(new_rule);
+            m_quantifiers.insert(new_rule, qs);
         }
     }
     
diff --git a/src/muz_qe/dl_mk_extract_quantifiers.h b/src/muz_qe/dl_mk_extract_quantifiers.h
index 512e386cd..4fc78c62c 100644
--- a/src/muz_qe/dl_mk_extract_quantifiers.h
+++ b/src/muz_qe/dl_mk_extract_quantifiers.h
@@ -37,6 +37,10 @@ namespace datalog {
 
         void extract(rule& r, rule_set& new_rules);
 
+        app_ref ensure_app(expr* e);
+
+        void ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail);
+
     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 227b1aee7..d5b495305 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -731,17 +731,15 @@ namespace pdr {
         TRACE("pdr", model_smt2_pp(tout, m, get_model(), 0););
         func_decl* f = p.head();
         unsigned arity = f->get_arity();
+        model_ref model = get_model_ptr();
         expr_ref_vector args(m);
-        func_decl_ref v(m);
+        expr_ref v(m);
+        model_evaluator mev(m);
+
         for (unsigned i = 0; i < arity; ++i) {
-            v = pm.o2n(p.sig(i),0);  
-            expr* e = get_model().get_const_interp(v);
-            if (e) {
-                args.push_back(e);
-            }
-            else {
-                args.push_back(m.mk_const(v));
-            }
+            v = m.mk_const(pm.o2n(p.sig(i),0));  
+            expr_ref e = mev.eval(model, v);
+            args.push_back(e);
         }            
         return expr_ref(m.mk_app(f, args.size(), args.c_ptr()), m);
     }
@@ -1833,7 +1831,7 @@ namespace pdr {
             pr = m.mk_asserted(m.mk_true());
             for (unsigned i = 0; i < vars.size(); ++i) {    
                 if (smt::is_value_sort(m, vars[i].get())) {
-                    VERIFY (M->eval(vars[i].get(), tmp, true)); 
+                    tmp = mev.eval(M, vars[i].get());
                     sub.insert(vars[i].get(), tmp, pr);
                 }
             }
@@ -1866,7 +1864,7 @@ namespace pdr {
                 for (unsigned j = 1; j < indices.size(); ++j) {
                     ptr_vector<app> const& vs = vars[indices[j]];
                     for (unsigned k = 0; k < vs.size(); ++k) {
-                        M->eval(vs[k]->get_decl(), tmp);
+                        tmp = mev.eval(M, vs[k]);
                         sub.insert(vs[k], tmp, pr);
                         child_states[indices[j]].push_back(m.mk_eq(vs[k], tmp));
                     }
diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp
index 8b5f6fa1e..04c189ca0 100644
--- a/src/muz_qe/pdr_quantifiers.cpp
+++ b/src/muz_qe/pdr_quantifiers.cpp
@@ -19,12 +19,13 @@ Revision History:
 
 #include "pdr_quantifiers.h"
 #include "pdr_context.h"
-#include "model_smt2_pp.h"
-#include "ast_smt2_pp.h"
 #include "qe.h"
 #include "var_subst.h"
 #include "dl_rule_set.h"
+#include "ast_smt2_pp.h"
 #include "model_smt2_pp.h"
+#include "ast_smt_pp.h"
+#include "expr_abstract.h"
 
 
 namespace pdr {
@@ -104,21 +105,34 @@ namespace pdr {
     }
      
     void quantifier_model_checker::apply_binding(quantifier* q, expr_ref_vector& binding) {          
+
+        datalog::scoped_no_proof _scp(m);
+
         app_ref_vector& var_inst = m_current_pt->get_inst(m_current_rule);
-        expr_substitution sub(m);
-        for (unsigned i = 0; i < var_inst.size(); ++i) {
-            expr* v = var_inst[i].get();
-            sub.insert(v, m.mk_var(i, m.get_sort(v)));
-        }
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-        rep->set_substitution(&sub);
+
+        TRACE("pdr", tout << mk_pp(q, m) << "\n";
+              tout << "binding\n";
+              for (unsigned i = 0; i < binding.size(); ++i) {
+                  tout << mk_pp(binding[i].get(), m) << " ";
+              }
+              tout << "\n";
+              tout << "inst\n";
+              for (unsigned i = 0; i < var_inst.size(); ++i) {
+                  tout << mk_pp(var_inst[i].get(), m) << " ";
+              }
+              tout << "\n";
+              );
+
+
         expr_ref e(m);
         var_subst vs(m, false);
+        inv_var_shifter invsh(m);
         vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
-        (*rep)(e);        
+        invsh(e, q->get_num_decls(), e);
+        expr_abstract(m, 0, var_inst.size(), (expr*const*)var_inst.c_ptr(), e, e);
+        TRACE("pdr", tout << mk_pp(e, m) << "\n";);
         m_instantiated_rules.push_back(m_current_rule);
         m_instantiations.push_back(to_app(e));
-        TRACE("pdr", tout << mk_pp(e, m) << "\n";);
     }
 
 
@@ -187,6 +201,7 @@ namespace pdr {
         expr_ref_vector fmls(m);
         front_end_params fparams;
         fparams.m_proof_mode = PGM_COARSE;
+        fparams.m_mbqi = true;
         // TBD: does not work on integers: fparams.m_mbqi = true;
 
         fmls.push_back(m_A.get());
@@ -364,6 +379,12 @@ namespace pdr {
               for (unsigned i = 0; i < m_Bs.size(); ++i) {
                   tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n";
               }
+              ast_smt_pp pp(m);
+              pp.add_assumption(m_A);
+              for (unsigned i = 0; i < m_Bs.size(); ++i) {
+                  pp.add_assumption(m_Bs[i].get());
+              }
+              pp.display_smt2(tout, m.mk_true());
               );
 
         find_instantiations(*qis, level);
@@ -406,6 +427,7 @@ namespace pdr {
                 m_quantifiers.remove(r);
                 datalog::rule_ref_vector rules(rule_m);
                 expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m);
+                std::cout << mk_pp(rule, m) << "\n";
                 rule_m.mk_rule(rule, rules, r->name());
                 for (unsigned i = 0; i < rules.size(); ++i) {
                     new_rules.add_rule(rules[i].get());
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 0fcb6c7c2..705b519a2 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -549,7 +549,7 @@ namespace pdr {
         }
     }
     
-    bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref else_case) {
+    bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
         SASSERT(m_array.is_array(a));
         
         while (m_array.is_store(a)) {
@@ -582,6 +582,9 @@ namespace pdr {
                 stores.push_back(store);
             }        
             else_case = g->get_else();
+            if (!else_case) {
+                return false;
+            }
             if (!is_ground(else_case)) {
                 return false;
             }
@@ -903,6 +906,32 @@ namespace pdr {
         return !has_x;
     }
 
+    expr_ref model_evaluator::eval(model_ref& model, expr* e) {
+        expr_ref result(m);
+        m_model = model;
+        VERIFY(m_model->eval(e, result, true));
+        if (m_array.is_array(e)) {
+            vector<expr_ref_vector> stores;
+            expr_ref_vector args(m);
+            expr_ref else_case(m);
+            if (extract_array_func_interp(result, stores, else_case)) {
+                result = m_array.mk_const_array(m.get_sort(e), else_case);
+                while (!stores.empty() && stores.back().back() == else_case) {
+                    stores.pop_back();
+                }
+                for (unsigned i = stores.size(); i > 0; ) {
+                    --i;
+                    args.resize(1);
+                    args[0] = result;
+                    args.append(stores[i]);
+                    result = m_array.mk_store(args.size(), args.c_ptr());
+                }
+                return result;
+            }
+        }
+        return result;
+    }
+
 
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
         ast_manager& m = fml.get_manager();
diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h
index bb9f74060..89598d347 100644
--- a/src/muz_qe/pdr_util.h
+++ b/src/muz_qe/pdr_util.h
@@ -103,7 +103,7 @@ namespace pdr {
         
         bool check_model(ptr_vector<expr> const & formulas);
 
-        bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref else_case);
+        bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);
         
     public:
         model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}
@@ -127,6 +127,8 @@ namespace pdr {
            for_each_expr visitor.
        */
        void operator()(expr* e) {} 
+
+       expr_ref eval(model_ref& mdl, expr* e);
     };
 
     /**