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

Fix bug reported at http://stackoverflow.com/questions/15226944/segmentation-fault-in-z3

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-05 09:04:03 -08:00
parent 9a4331995e
commit bdc675b1df
3 changed files with 18 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -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://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 Version 4.3.1
============= =============

11
src/ast/macros/macro_util.cpp
View file

@ -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 is_hint_head(head, vars) must also return true
*/ */
bool macro_util::is_poly_hint(expr * n, app * head, expr * exception) { 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" 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";); if (exception) tout << mk_pp(exception, m_manager); else tout << "<null>";
tout << "\n";);
ptr_buffer<var> vars; ptr_buffer<var> vars;
if (!is_hint_head(head, vars)) { if (!is_hint_head(head, vars)) {
TRACE("macro_util_hint", tout << "failed because head is not hint head\n";); TRACE("macro_util_hint", tout << "failed because head is not hint head\n";);
@ -792,6 +793,9 @@ 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); mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest);
expr_ref def(m_manager); expr_ref def(m_manager);
mk_sub(rhs, rest, def); mk_sub(rhs, rest, def);
// 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); 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)) { else if (is_times_minus_one(arg, neg_arg) && is_app(neg_arg)) {
@ -810,6 +814,9 @@ 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); mk_add(args.size(), args.c_ptr(), m_manager.get_sort(arg), rest);
expr_ref def(m_manager); expr_ref def(m_manager);
mk_sub(rest, rhs, def); mk_sub(rest, rhs, def);
// 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); add_arith_macro_candidate(to_app(neg_arg), num_decls, def, atom, is_ineq, _is_poly_hint, r);
} }
} }

5
src/model/model_v2_pp.cpp
View file

@ -80,3 +80,8 @@ void model_v2_pp(std::ostream & out, model_core const & md, bool partial) {
display_constants(out, md); display_constants(out, md);
display_functions(out, md, partial); display_functions(out, md, partial);
} }
// debugging support
void pp(model_core const & md) {
model_v2_pp(std::cout, md, false);
}