From ead39ea6c5cb0da995fd6559dc9326c5699d0f66 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Nov 2012 10:49:58 -0800 Subject: [PATCH] Fixed bug reported by Nuno Lopes Signed-off-by: Leonardo de Moura --- src/ast/ast.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 6763d1d55..3c98dca33 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1814,6 +1814,11 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co } } else { + if (decl->get_arity() != num_args) { + // Invalid input: unexpected number of arguments for non-associative operator. + // So, there is no point in coercing the input arguments. + return false; + } for (unsigned i = 0; i < num_args; i++) { sort * d = decl->get_domain(i); if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i]))