How to change the type of ArithRef type to Integer type so that can be used as array indices?

[debarpita23-2024]

I have written a piece of code in SMT solver Z3 (in Python). The code is as follows:

from z3 import *
from numpy import * 

x=Int('x')
y=Int('y')

s= Solver()

s.add(y==8)

arr  = [ [ Bool("arr_%s_%s" % (i, j)) for j in range(5) ]         
      for i in range(2) ]

test = [ [ Bool("test_%s_%s" % (i, j)) for j in range(5) ]         
      for i in range(2) ]

s.add(test[0][0]==False, test[0][1]==True, test[0][2]==True, test[0][3]==False, test[0][4]==True, arr[0][0]==True)

for j in range(9):
    s.add( And ( x == ((j+1)/y),
                 If ( test[0][x]==True,
                      arr[0][j+1]==False,
             arr[0][j+1] == True  ))
      )

print (s.check())
if s.check() == sat:
    m = s.model()
    r = [m.evaluate(arr[0][j]) for j in range(10) ]
    print_matrix(r)

After running the code the output is:

Traceback (most recent call last):
  File "d:\d\Research Work ISI\Ericsson\Implementation with SMT\Untitled-1.py", line 21, in <module>
    If ( test[0][x]==True,
         ~~~~~~~^^^
TypeError: list indices must be integers or slices, not ArithRef

I want a solution to this problem. 'x' here is declared as Integer. I am calculating value of 'x' each time in the for loop and based on that the array 'arr' is updated. Now it is being displayed in the terminal that 'x' is Arithref, so cannot be used as list index. Is there a possible way to change its type to Integer? I was trying with commands: cast(x) , IntSort().cast(x), but it is not working.