From bdc675b1dfef87fcffeb7f3e5143128492d3bd89 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Mar 2013 09:04:03 -0800 Subject: [PATCH] Fix bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/ast/macros/macro_util.cpp | 15 +++++++++++---- src/model/model_v2_pp.cpp | 5 +++++ 3 files changed, 18 insertions(+), 4 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 7aaaf2f8d..643c9b26f 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -63,6 +63,8 @@ Version 4.3.2 - Fixed bug reported at http://z3.codeplex.com/workitem/23 (Thanks to Paul Jackson). +- Fixed bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 (Thanks to Tianhai Liu). + Version 4.3.1 ============= diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index e9b9c831e..bd21aa1ac 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -597,8 +597,9 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref is_hint_head(head, vars) must also return true */ bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { - TRACE("macro_util_hint", tout << "is_poly_hint n:\n" << mk_pp(n, m_manager) << "\nhead:\n" << mk_pp(head, m_manager) << "\nexception:\n" - << mk_pp(exception, m_manager) << "\n";); + TRACE("macro_util_hint", tout << "is_poly_hint n:\n" << mk_pp(n, m_manager) << "\nhead:\n" << mk_pp(head, m_manager) << "\nexception:\n"; + if (exception) tout << mk_pp(exception, m_manager); else tout << ""; + tout << "\n";); ptr_buffer vars; if (!is_hint_head(head, vars)) { TRACE("macro_util_hint", tout << "failed because head is not hint head\n";); @@ -792,7 +793,10 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest); expr_ref def(m_manager); mk_sub(rhs, rest, def); - add_arith_macro_candidate(to_app(arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); + // If is_poly_hint, rhs may contain variables that do not occur in to_app(arg). + // So, we should re-check. + if (!_is_poly_hint || is_poly_hint(def, to_app(arg), 0)) + add_arith_macro_candidate(to_app(arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); } else if (is_times_minus_one(arg, neg_arg) && is_app(neg_arg)) { f = to_app(neg_arg)->get_decl(); @@ -810,7 +814,10 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest); expr_ref def(m_manager); mk_sub(rest, rhs, def); - add_arith_macro_candidate(to_app(neg_arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); + // If is_poly_hint, rhs may contain variables that do not occur in to_app(neg_arg). + // So, we should re-check. + if (!_is_poly_hint || is_poly_hint(def, to_app(neg_arg), 0)) + add_arith_macro_candidate(to_app(neg_arg), num_decls, def, atom, is_ineq, _is_poly_hint, r); } } } diff --git a/src/model/model_v2_pp.cpp b/src/model/model_v2_pp.cpp index 9073ddece..4600ccc9e 100644 --- a/src/model/model_v2_pp.cpp +++ b/src/model/model_v2_pp.cpp @@ -80,3 +80,8 @@ void model_v2_pp(std::ostream & out, model_core const & md, bool partial) { display_constants(out, md); display_functions(out, md, partial); } + +// debugging support +void pp(model_core const & md) { + model_v2_pp(std::cout, md, false); +}