diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index a4bc4de6d..e19b9fef8 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -315,7 +315,7 @@ private:
         if (m_params.get_bool(":print-certificate", false)) {
             datalog::context& dlctx = m_dl_ctx->dlctx();
             if (!dlctx.display_certificate(ctx.regular_stream())) {
-                throw cmd_exception("certificates are not supported for selected DL_ENGINE");
+                throw cmd_exception("certificates are not supported for the selected engine");
             }
             ctx.regular_stream() << "\n";
         }
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 81826daec..9a5f7280c 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -1523,7 +1523,7 @@ namespace datalog {
         switch(get_engine()) {
         case DATALOG_ENGINE:            
             return false;
-        case PDR_ENGINE: 
+        case QPDR_ENGINE: 
             ensure_pdr();
             m_pdr->display_certificate(out);
             return true;
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index f92a56a4f..1d3d62020 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -194,6 +194,7 @@ namespace datalog {
         }
     }
 
+    // TBD: replace by r.has_quantifiers() and test
     bool mk_rule_inliner::has_quantifier(rule const& r) const {
         unsigned utsz = r.get_uninterpreted_tail_size();
         for (unsigned i = utsz; i < r.get_tail_size(); ++i) {
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 1f1d12340..2ff341e07 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -818,6 +818,11 @@ namespace datalog {
     }
 
     rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) {        
+        for (unsigned i = 0; i < src.get_num_rules(); ++i) {
+            if (src.get_rule(i)->has_quantifiers()) {
+                return 0;
+            }
+        }
         ref<slice_proof_converter> spc;
         ref<slice_model_converter> smc;
         if (pc) {