[Feature Request] Tuples in Z3 DSL

[rah4927]

Some functions can be multiple output. For example the gcd algorithm (a, b) -> (a - b, b), so would be nice to have an abstraction for tuples in the DSL. @amit9oct