# Z3 is unable to predict the operand

When I try to solve this crackme chall (https://crackmes.one/crackme/61ffb07c33c5d46c8bcbfc1d) , there is a condition that I can't bypass and my z3 script can't predict the input string that will bypass the condition

and this is my z3 script

``````from z3 import *

v7 = [123,456,789,987,654,321]
v6 = [92,29,380,2,497,296]

s = [BitVec(f'a{i}', 8) for i in range(5)]

solver = Solver()

v20 = 0x7FFFFFFF
for i in range(5):
v20 += i * s[i]

solver.check()
``````
• The function has much more logic and you need to add that in the script too Apr 22 at 14:02

It is to note that the division in the binary is unsigned while according to doc

Use the function URem() for unsigned remainder, and SRem() for signed remainder.

`%` operator by default is an alias for `SRem` or signed modulo. You need to use `URem`. I have fixed your logic as well in this code

``````from z3 import *

v7 = [123,456,789,987,654,321]
v6 = [92,29,380,2,497,296]
arrl = 14
argv1 = [BitVec(f'a{i}', 32) for i in range(arrl)]

solver = Solver()
v18 = BitVecVal(0x7fffffff, 32)

for i in range(arrl):
v18 += i*argv1[i]

for i in range(6):
• Thanks! as you see there is `if ( ((unsigned int (__fastcall *)(char *, size_t))v14)(a2[1], v5) )` in decompiled code, can you explain what this check do ? and what does this mean `(unsigned int (__fastcall *)(char *, size_t))` ? Apr 22 at 18:36