diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 59efb2a89..2881f1b62 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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);