mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2012-11-23 19:25:19 +00:00
commit 6834abd781
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]))