Simplification yields f/n applied to x₁...xₘ with m≠n

[janvrany]

I noticed that simplification sometimes yields an application AST with more children than corresponding function declaration arity. For example:

from z3 import BitVec, simplify

a = BitVec('a', 8)
b = BitVec('b', 8)
c = BitVec(1, 8)

original = a + b + c
simplified = simplify(original)

assert original.decl().arity() == len(original.children())
assert simplified.decl().arity() == len(simplified.children())

Here the first assertion holds, the second does not, because simplified.decl().arity() is 2 whereas simplified has 3 children (a, b and c).

I'd intuitively expect that number of application arguments is always the same as corresponding function declarations' arity.

[NikolajBjorner]

you will have to configure

set_param("rewriter.flat", false)

The parameter was ignored in an optimizaton that flattens function applications that occur only with single reference count.