# Z3 and If-logic

Z3 is a fantastic tool which helped me a lot! But sometimes I'm stuck on the binary code which implements custom If-logic. Recursive factorial function is good example of it:

``````def fact(x):
if x == 1:
return 1
else:
return x * fact(x - 1)
``````

I'm aware of the fact Z3 python has `If()` function but it can only switch between two values.

Here is example of simple keygen-me which I wrote to illustrate this problem. Is there a way to solve it cleanly with Z3?

``````import sys

def fact(x):
if x == 1:
return 1
else:
return x * fact(x - 1)

def check_serial(s):

for i in range(len(s)):
if s[i] < 10:
print("[!] poor serial number")
exit(0)

facts = [fact(s[i]) for i in range(len(s))]

xor = 0
for i in range(len(s)):
xor = xor ^ facts[i]

return xor

if len(sys.argv) != 9:
print("[!] Usage: %s x x x x x x x x, where is number > 10" % sys.argv[0])
exit(0)

nums = [int(x) for x in sys.argv[1:]]

if check_serial(nums) == 0x3fb4b7f405d4fb5e2a6740000:
print("[+] serial number is valid, congratz!")
else:
print("[!] serial number is invalid")
``````
• z3 is not very good with recursive function. You can find similar questions on SO – Paweł Łukasik Oct 17 '19 at 14:25