From ccf10d0abe86c86c66bc5e7908d3f5deda042d10 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 25 May 2013 14:38:02 -0700
Subject: [PATCH 1/2] fix crash in PDR engine when transformations don't
 produce output predicates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/dl_mk_slice.cpp      | 6 ++++++
 src/muz_qe/pdr_dl_interface.cpp | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 1a97c1b81..5b9d43acc 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -710,6 +710,7 @@ namespace datalog {
     void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) {
         obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end();
         ptr_vector<sort> domain;
+        bool has_output = false;
         func_decl* f;
         for (; it != end; ++it) {
             domain.reset();
@@ -731,8 +732,13 @@ namespace datalog {
             }
             else if (src.is_output_predicate(p)) {
                 dst.set_output_predicate(p);
+                has_output = true;
             }
         }
+        // disable slicing if the output predicates don't occur in rules.
+        if (!has_output) {
+            m_predicates.reset();
+        }
     }
 
     bool mk_slice::rule_updated(rule const& r) {
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 3ff54e68e..437c08f6a 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -133,6 +133,12 @@ lbool dl_interface::query(expr * query) {
             --num_unfolds;
         }
     }
+
+    if (m_ctx.get_rules().get_output_predicates().empty()) {
+        m_context->set_unsat();
+        return l_false;
+    }
+
     query_pred = m_ctx.get_rules().get_output_predicate();
 
     IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););

From 7c12ab47165a88ab514c8cddcf65b1be6e784ec8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 25 May 2013 14:40:57 -0700
Subject: [PATCH 2/2] fix some compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/aig_exporter.cpp | 2 ++
 src/muz_qe/clp_context.cpp  | 3 ++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/muz_qe/aig_exporter.cpp b/src/muz_qe/aig_exporter.cpp
index 1d6ef3633..ca0030fc3 100755
--- a/src/muz_qe/aig_exporter.cpp
+++ b/src/muz_qe/aig_exporter.cpp
@@ -265,6 +265,8 @@ namespace datalog {
 
         case AST_VAR:
             return get_var(e);
+        default:
+            UNREACHABLE();
         }
         
         UNREACHABLE();
diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp
index 5dd6fb9d8..94a956eb9 100644
--- a/src/muz_qe/clp_context.cpp
+++ b/src/muz_qe/clp_context.cpp
@@ -66,8 +66,9 @@ namespace datalog {
             m_ctx.ensure_opened();
             m_solver.reset();
             m_goals.reset();
-            func_decl *head_decl = rm.mk_query(query, m_ctx.get_rules());
+            rm.mk_query(query, m_ctx.get_rules());
             m_ctx.apply_default_transformation();
+            func_decl *head_decl = m_ctx.get_rules().get_output_predicate();
 
             expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
             ground(head);