Equivalent to CVC5's ADT update constructor

[nblei]

CVC5 supports the (_ update <adt-field-identifier>) : <algebraic-datatype> -> <field-type> -> <algebraic-datatype> ADT constructor which, as far as I can tell, is not part of the SMTLIB 2.6 standard.

This is useful for ADTs which are being used in a way similar to a structure in an imperative language, since structures may have many fields and thus using standard constructors is tedious.

Is there a similar ADT mutator / update-constructor supported by z3?

[NikolajBjorner]

It was introduced a while ago in z3. It is called:

(_ update-field <adt-field-identifier>)

[nblei]

Thanks!