diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index eced4c128..ec723b531 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -25,7 +25,7 @@ Revision History:
 #include "dl_mk_rule_inliner.h"
 #include "dl_rule.h"
 #include "dl_rule_transformer.h"
-#include "dl_mk_extract_quantifiers.h"
+//include "dl_mk_extract_quantifiers.h"
 #include "smt2parser.h"
 #include "pdr_context.h"
 #include "pdr_dl_interface.h"
@@ -146,7 +146,7 @@ lbool dl_interface::query(expr * query) {
             --num_unfolds;
         }
     }
-
+#if 0
     // remove universal quantifiers from body.
     datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
     datalog::rule_transformer extract_q_tr(m_ctx);
@@ -186,6 +186,8 @@ lbool dl_interface::query(expr * query) {
             return result;
         }
     }
+#endif
+    return l_undef;
 }
 
 expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {