mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-07-14 12:08:34 -07:00
commit 31eb738db5
4 changed files with 16 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast.cpp
View file

@ -2046,8 +2046,14 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
}
app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
if (decl->get_arity() != num_args && !decl->is_right_associative() &&
!decl->is_left_associative() && !decl->is_chainable()) {
bool type_error =
decl->get_arity() != num_args && !decl->is_right_associative() &&
!decl->is_left_associative() && !decl->is_chainable();
type_error |= (decl->get_arity() != num_args && num_args < 2 &&
decl->get_family_id() == m_basic_family_id && !decl->is_associative());
if (type_error) {
std::ostringstream buffer;
buffer << "Wrong number of arguments (" << num_args
<< ") passed to function " << mk_pp(decl, *this);