diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index f38999381..77b391ef7 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -338,7 +338,7 @@ namespace datalog {
 
     expr_ref context::bind_variables(expr* fml, bool is_forall) {
         expr_ref result(m);
-        app_ref_vector & vars = m_vars;
+        app_ref_vector const & vars = m_vars;
         if (vars.empty()) {
             result = fml;
         }
@@ -352,13 +352,20 @@ namespace datalog {
             else {
                 svector<symbol> names;
                 for (unsigned i = 0; i < sorts.size(); ++i) {
-                    if (vars.size() == i) {
-                        vars.push_back(m.mk_fresh_const("x", m.mk_bool_sort()));
-                    }
                     if (!sorts[i]) {
-                        sorts[i] = vars[i]->get_decl()->get_range();
+                        if (i < vars.size()) { 
+                            sorts[i] = vars[i]->get_decl()->get_range();
+                        }
+                        else {
+                            sorts[i] = m.mk_bool_sort();
+                        }
+                    }
+                    if (i < vars.size()) {
+                        names.push_back(vars[i]->get_decl()->get_name());
+                    }
+                    else {
+                        names.push_back(symbol(i));
                     }
-                    names.push_back(vars[i]->get_decl()->get_name());
                 }
                 quantifier_ref q(m);
                 sorts.reverse();
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 0840f1d73..2c009dc25 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -119,7 +119,6 @@ namespace pdr {
         select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {}        
     };
 
-    template class rewriter_tpl<select_elim_cfg>;
 
     class select_elim_star : public rewriter_tpl<select_elim_cfg> {
         select_elim_cfg m_cfg;
@@ -1205,5 +1204,6 @@ namespace pdr {
 
 template class rewriter_tpl<pdr::ite_hoister_cfg>;
 
+template class rewriter_tpl<pdr::select_elim_cfg>;