mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix type checking for non-associative basic operations, fixes issue #160
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
21201371ed
commit
e13bf2424e
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue