How to declare an array with mixed data types in Z3?

I am using the python API for z3 and my goal is to be able to reason about sequences containing one of two kinds of data: either an integer or my custom data type, which does not have any properties other than being a type. I read about 'DeclareSort' which seems to mean we can create a custom type. So I used it as follows:

ct = DeclareSort('CT')
CT = Const('CT', ct)

Then I tried to create a union type between my type and integers as follows:

u = Datatype('IntOrCT')
u.declare('IntV', ('int', IntSort()))
u.declare('CTV', ('ct', ct))

IntOrCT = u.create()
CTV = IntOrCT.CTV
IntV = IntOrCT.IntV

I am now trying to use them in an array. However, I cannot add any integers to my arrays and get: z3.z3types.Z3Exception: Z3 expression expected

# X = Array('x', IntOrCT, IntOrCT)
# Store(X, 0, 4)

If I change IntOrCT to IntSort(), it will work. Is there any idea what could be missing from the code? or is what I'm trying to do not possible in z3?

Solution

You created an array indexed by IntOrCT, storing IntOrCT values; so you need to wrap your index and values in the corresponding constructors:

X = Array('x', IntOrCT, IntOrCT)
print(Store(X, IntV(0), IntV(4)))

When I run this, I get:

Store(x, IntV(0), IntV(4))