From 64e2011d425cc3493468eba862f309815263538b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 24 Feb 2015 17:34:38 -0800
Subject: [PATCH] fix crash in explanation generation. Codeplex issue 181

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_rule.cpp            | 5 +++--
 src/muz/rel/dl_mk_explanations.cpp  | 2 +-
 src/muz/rel/dl_relation_manager.cpp | 1 +
 src/muz/rel/karr_relation.h         | 2 +-
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 017bac724..1849903c5 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -884,14 +884,15 @@ namespace datalog {
     struct uninterpreted_function_finder_proc {
         ast_manager& m;
         datatype_util m_dt;
+        dl_decl_util  m_dl;
         bool m_found;
         func_decl* m_func;
         uninterpreted_function_finder_proc(ast_manager& m): 
-            m(m), m_dt(m), m_found(false), m_func(0) {}
+            m(m), m_dt(m), m_dl(m), m_found(false), m_func(0) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) { }
         void operator()(app * n) {
-            if (is_uninterp(n)) {
+            if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) {
                 m_found = true;
                 m_func = n->get_decl();
             }
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 60a10190a..7344f187c 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -828,7 +828,7 @@ namespace datalog {
             SASSERT(&expl_singleton->get_plugin()==m_er_plugin);
             m_e_fact_relation = static_cast<explanation_relation *>(expl_singleton);
         }
-        func_decl_set const& predicates = m_context.get_predicates();
+        func_decl_set predicates(m_context.get_predicates());
         decl_set::iterator it = predicates.begin();
         decl_set::iterator end = predicates.end();
         for (; it!=end; ++it) {
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 9421b26df..7fcca9ce2 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -734,6 +734,7 @@ namespace datalog {
 
     relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src, 
             const relation_base * delta) { 
+        TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << "\n";); 
         relation_union_fn * res = tgt.get_plugin().mk_union_fn(tgt, src, delta);
         if(!res && &tgt.get_plugin()!=&src.get_plugin()) {
             res = src.get_plugin().mk_union_fn(tgt, src, delta);
diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h
index 00a92748a..72448f026 100644
--- a/src/muz/rel/karr_relation.h
+++ b/src/muz/rel/karr_relation.h
@@ -45,7 +45,7 @@ namespace datalog {
         {}            
         
         virtual bool can_handle_signature(const relation_signature & sig) {
-            return true;
+            return get_manager().get_context().karr();
         }
 
         static symbol get_name() { return symbol("karr_relation"); }