mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

check for non-nullness when handling optional info fields for marking. Fixes issue #719

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-08-23 11:33:40 -03:00
parent 879f792125
commit 0a09d5ff52
2 changed files with 19 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast.cpp
View file

@ -1430,14 +1430,22 @@ ast_manager::~ast_manager() {
for (; it_a != end_a; ++it_a) {
ast* n = (*it_a);
switch (n->get_kind()) {
case AST_SORT:
mark_array_ref(mark, to_sort(n)->get_info()->get_num_parameters(), to_sort(n)->get_info()->get_parameters());
case AST_SORT: {
sort_info* info = to_sort(n)->get_info();
if (info != 0) {
mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
}
break;
case AST_FUNC_DECL:
mark_array_ref(mark, to_func_decl(n)->get_info()->get_num_parameters(), to_func_decl(n)->get_info()->get_parameters());
}
case AST_FUNC_DECL: {
func_decl_info* info = to_func_decl(n)->get_info();
if (info != 0) {
mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
}
mark_array_ref(mark, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
mark.mark(to_func_decl(n)->get_range(), true);
break;
}
case AST_APP:
mark.mark(to_app(n)->get_decl(), true);
mark_array_ref(mark, to_app(n)->get_num_args(), to_app(n)->get_args());

9
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -44,6 +44,9 @@ namespace datalog {
if (m_context.has_facts(r->get_decl(i))) {
return 0;
}
if (false && r->is_neg_tail(i)) {
return 0;
}
if (r->is_neg_tail(i)) {
if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
if (!new_tail) {
@ -53,11 +56,13 @@ namespace datalog {
}
new_tail = true;
}
} else if (new_tail) {
}
else if (new_tail) {
m_new_tail.push_back(r->get_tail(i));
m_new_tail_neg.push_back(true);
}
} else {
}
else {
SASSERT(!new_tail);
if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
contained = false;