How to write constraint to find max value among n variable

[dannyjpereira]

Dear sir,
I am trying to formulate SMT constraints for max operation among n variable.
max(a1,a2,.....an)
How can we specify this function in Z3py?
Help in this regard is appreciated.

[NikolajBjorner]

1. Use nested if-then-else: max(x, y) = (if (> x y) x y)
2. Use a fresh variable that is an upper bound for a1, ..., an, assert max_x >= a1, max_x >= a2, ...
   3