mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Fixed bug reported by Nuno Lopes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-23 10:49:58 -08:00
parent edc9dccbcf
commit ead39ea6c5
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/ast.cpp
View file

@ -1814,6 +1814,11 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co
} }
} }
else { 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++) { for (unsigned i = 0; i < num_args; i++) {
sort * d = decl->get_domain(i); sort * d = decl->get_domain(i);
if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i])) if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i]))