[Python] TypeError: 'Artihref' object is not iterable z3-solver

I am trying to create a function called nochange which keeps the variable passed through within the same transition state it was already in.

variables = [('pc_thrd1', 'int'), ('pc_thrd2', 'int'), ('flag1', 'int'), ('flag2', 'int'), ('x', 'int'), ('turn', 'int'), ('pid', 'int')]
variables_enc_0, variables_enc_1 = bmchecker.add_variables(variables)

#aliases of state variables
pc_thrd1 = variables_enc_0[0]
pc_thrd2 = variables_enc_0[1]
flag1 = variables_enc_0[2]
flag2 = variables_enc_0[3]
x = variables_enc_0[4]
turn = variables_enc_0[5]
pid = variables_enc_0[6]
pc_thrd1_x = variables_enc_1[0]
pc_thrd2_x = variables_enc_1[1]
flag1_x = variables_enc_1[2]
flag2_x = variables_enc_1[3]
x_x = variables_enc_1[4]
turn_x = variables_enc_1[5]

state0_enc = And(Or(x == 0, x == 1), (flag1 == 0), (flag2 == 0), (turn == 0), (pc_thrd1 == 0), (pc_thrd2 == 0), (pid == 0))

bmchecker.add_initial_state_enc(state0_enc)
def nochange(l):
c = None
for i in l:
x, y = i
if c is None:
c = (x == y)
else:
c = And(x == y, (c))
return c


I then created this variable calling in the function on the int variables

thr1 = Or(And(pc_thrd1 == 0, flag1_x == 1, pc_thrd1_x == 1, nochange(flag2), nochange(flag2_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 1, flag2 < 1, pc_thrd1 == 6, nochange(flag1), nochange(flag1_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 1, flag2 >= 1, pc_thrd1_x == 2, nochange(flag1), nochange(flag1_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 2, turn == 0, pc_thrd1_x == 6, nochange(flag2), nochange(flag2_x), nochange(flag1), nochange(flag1_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 2, Not(turn == 0), pc_thrd1 == 3, nochange(flag2), nochange(flag2_x), nochange(flag1), nochange(flag1_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 3, flag2 == 0, pc_thrd1 == 4, nochange(flag1), nochange(flag1_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 4, turn == 0, pc_thrd1 == 5, nochange(flag2), nochange(flag2_x), nochange(flag1), nochange(flag1_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 4, Not(turn == 0), pc_thrd1 == 4, nochange(flag2), nochange(flag2_x), nochange(flag1), nochange(flag1_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 5, flag1 == 1, pc_thrd1 == 6, nochange(flag2), nochange(flag2_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 6, x == 0, pc_thrd1 == 7, nochange(flag2), nochange(flag2_x), nochange(turn), nochange(turn_x), nochange(flag1), nochange(flag1_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 7, turn == 1, pc_thrd1 == 8, nochange(flag2), nochange(flag2_x), nochange(flag1), nochange(flag1_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
And(pc_thrd1 == 8, flag1 == 0, pc_thrd1 == 0, nochange(flag2), nochange(flag2_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)))

all_thrds = And(And(0<=pid, pid<=1),
Or(And(pid == 0, turn == 1, thr1, pc_thrd2 == pc_thrd2_x),
And(pid == 1, turn == 0, pc_thrd1 == pc_thrd1_x)))


I expected to receive an error trace print which would allow me to create a finite state machine however I recieved this syntax error

File "c:\Users\madom\Python projects\Bounded_Model_Check\Prof_Z_example\MultiThread_1.py", line 82, in <module>
thr1 = Or(And(pc_thrd1 == 0, flag1_x == 1, pc_thrd1_x == 1, nochange(flag2), nochange(flag2_x), nochange(turn), nochange(turn_x), nochange(x), nochange(x_x), nochange(pc_thrd2), nochange(pc_thrd2_x)),
File "c:\Users\madom\Python projects\Bounded_Model_Check\Prof_Z_example\MultiThread_1.py", line 73, in nochange
for i in l:
TypeError: 'ArithRef' object is not iterable


In essence, thr1 is a set of constraints for a thread represented by C Code which I did not think I needed to add, the nochange function is supposed to manipulate any transitory state, for example, flag1, flag1_x would remain equal to whatever value it was equal too and then that would get passed through Z3 to allow me to find a suitable model.

Continue reading...