I am quite sure that it should be possible to describe tuples using SMT-lib syntax, especially for the Z3 solver. However, I can't really find a way of doing so. The only thing I found is this documentation page, but I don't get how to use it in z3 -in.
My struggles so far:
(declare-const t (Prod Int Bool))
(error "line 1 column 19: unknown sort 'Prod'")
(declare-const t (Tuple Int Bool))
(error "line 2 column 18: unknown sort 'Tuple'")
(declare-const t (Pair Int Bool))
(error "line 3 column 18: unknown sort 'Pair'")
In addition to what Christoph said, there's an example right in the SMTLib document: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
In Section 4.2.3, you can find:
(declare-datatype Pair (par (X Y) ((pair (first X) (second Y)))))
If you just want IntxBool, then you can simplify:
(declare-datatype PairIntBool (par () ((pair (first Int) (second Bool)))))
In general, you should read through Section 4.2.3 to learn about how to declare and use new data-types.