From a9e8045071cb5a172cadf111244cbb5f8fb16f36 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 Mar 2014 20:23:54 -0700
Subject: [PATCH] fix bug reported by Nuno Lopes when query gets sliced

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/bmc/dl_bmc_engine.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 7a88c1188..0dcbf4644 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -1465,6 +1465,10 @@ namespace datalog {
         if (m_rules.get_num_rules() == 0) {
             return l_false;
         }
+        if (m_rules.get_predicate_rules(m_query_pred).empty()) {
+            return l_false;
+        }
+
 
         if (is_linear()) {
             if (m_ctx.get_engine() == QBMC_ENGINE) {