does Z3_mk_datatype write to the constructors argument?

[bakkot]

In the api, the last parameter to Z3_mk_datatype is marked as being _inout_array. Does that mean it writes to that array, as well as reading from it? I'm trying to figure out if I need to handle that case specially in the JS bindings - in all other cases array arguments are either only read from or written to.

If not, what does it mean?

Sorry I couldn't figure this out myself by reading the source; my C++ is rusty.

[NikolajBjorner]

in-out-array: The elements of the array are initialized (with pointers). Then the function reads those elements and change (write) their state. In the two functions that use inout_array the elements don't change. They stay the same, but their internal state is changed. It is extremely unlikely the behavior will change. In fact other API wrapper build in this assumption. So you should be able to assume that the elements are unchanged.
in-array: the elements are read by the function, but not changed.
out-array: the elements are un-initialized and they are set by the function.

With this behavior you may be able to treat inout_array as just in_array.