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

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

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 4a51da9b0..1a8e42704 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1199,6 +1199,7 @@ void cmd_context::reset(bool finalize) {
     restore_assertions(0);
     if (m_solver)
         m_solver = 0;
+    m_scopes.reset();
     m_opt = 0;
     m_pp_env = 0;
     m_dt_eh  = 0;
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 6aa6d5ea5..6d1f6664a 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -335,6 +335,7 @@ namespace datalog {
         if (!is_predicate(decl)) {
             m_pinned.push_back(decl);
             m_preds.insert(decl);
+            TRACE("dl", tout << mk_pp(decl, m) << "\n";);
             if (named) {
                 m_preds_by_name.insert(decl->get_name(), decl);
             }
@@ -345,6 +346,7 @@ namespace datalog {
         m_preds.reset();
         func_decl_set::iterator it = preds.begin(), end = preds.end();
         for (; it != end; ++it) {
+            TRACE("dl", tout << mk_pp(*it, m) << "\n";);
             m_preds.insert(*it);
         }
     }
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 55c87f66e..b108df1bc 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -828,11 +828,13 @@ 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) {
             func_decl * orig_decl = *it;
+            TRACE("dl", tout << mk_pp(orig_decl, m_manager) << "\n";);
             func_decl * e_decl = get_e_decl(orig_decl);
 
             if (!rmgr.try_get_relation(orig_decl) &&
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index a2b16bcf9..0dd62b544 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -755,7 +755,7 @@ namespace datalog {
 
 
     relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src, 
-            const relation_base * delta) { 
+            const relation_base * delta) {         
         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);