From 2a286541e00230025af208bc5dbfccaefb4ba7a1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Dec 2012 08:36:25 -0800 Subject: [PATCH] Fix crash reported at http://z3.codeplex.com/workitem/11. Fix array rewriter bug, rewriter was producing sort incorrect expression. Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/ast/array_decl_plugin.cpp | 13 ++++++------- src/ast/rewriter/array_rewriter.cpp | 9 ++++++++- 3 files changed, 16 insertions(+), 8 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 694a6d635..104828a45 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -51,6 +51,8 @@ Version 4.3.2 - Fixed timers on Linux and FreeBSD. +- Fixed crash reported at http://z3.codeplex.com/workitem/11. + Version 4.3.1 ============= diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 857cec105..47842ae90 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -113,15 +113,14 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * m_manager->raise_exception("invalid const array definition, invalid domain size"); return 0; } - unsigned num_parameters = s->get_num_parameters(); - - if (num_parameters == 0) { - m_manager->raise_exception("parameter mismatch"); + if (!is_array_sort(s)) { + m_manager->raise_exception("invalid const array definition, parameter is not an array sort"); + return 0; + } + if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) { + m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument"); return 0; } - - // TBD check that range sort corresponds to last parameter. - parameter param(s); func_decl_info info(m_family_id, OP_CONST_ARRAY, 1, ¶m); info.m_private_parameters = true; diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 9dbbeb231..0bb7378f4 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -292,7 +292,14 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c } expr * fv = m().mk_app(f, values.size(), values.c_ptr()); - parameter p(m().get_sort(args[0])); + sort * in_s = get_sort(args[0]); + ptr_vector domain; + unsigned domain_sz = get_array_arity(in_s); + for (unsigned i = 0; i < domain_sz; i++) + domain.push_back(get_array_domain(in_s, i)); + sort_ref out_s(m()); + out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range()); + parameter p(out_s.get()); result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv); return BR_REWRITE2; }