mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-05 01:27:41 +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:34:38 -08:00
parent 8ea7a1905f
commit 64e2011d42
4 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/base/dl_rule.cpp
View file

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