mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix crash in explanation generation. Codeplex issue 181

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-02-24 17:03:34 -08:00
parent c3232693f0
commit b8fbc32689
4 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cmd_context/cmd_context.cpp
View file

@ -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;

2
src/muz/base/dl_context.cpp
View file

@ -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);
}
}

4
src/muz/rel/dl_mk_explanations.cpp
View file

@ -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) &&

2
src/muz/rel/dl_relation_manager.cpp
View file

@ -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);