From e13bf2424e9641fb9e0c38ed626ebad8239a1723 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 08:29:24 -0700 Subject: [PATCH] fix type checking for non-associative basic operations, fixes issue #160 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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);