diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index cc2dc02c5..7eed67ff0 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -675,9 +675,11 @@ namespace datalog {
         case PDR_ENGINE:
             check_existential_tail(r);
             check_positive_predicates(r);
+            check_uninterpreted_free(r);
             break;
         case QPDR_ENGINE:
             check_positive_predicates(r);
+            check_uninterpreted_free(r);
             break;
         case BMC_ENGINE:
             check_positive_predicates(r);
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 35af38630..f6965b084 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -223,6 +223,7 @@ public:
         dlctx.updt_params(m_params);
         unsigned timeout   = m_dl_ctx->get_params().timeout(); 
         cancel_eh<datalog::context> eh(dlctx);
+        bool query_exn = false;
         lbool status = l_undef;
         {
             scoped_ctrl_c ctrlc(eh);
@@ -237,6 +238,7 @@ public:
             }
             catch (z3_exception& ex) {
                 ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;
+                query_exn = true;
             }
         }
         switch (status) {
@@ -269,7 +271,7 @@ public:
                 break;
 
             case datalog::OK: 
-                UNREACHABLE();
+                SASSERT(query_exn);
                 break;
 
             case datalog::CANCELED: