Z3 是一个很棒的工具，对我帮助很大！但有时我被困在实现自定义 If 逻辑的二进制代码上。递归阶乘函数就是一个很好的例子：

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

我知道 Z3 python 有If()函数但它只能在两个值之间切换。

这是我编写的用于说明此问题的简单 keygen-me 示例。有没有办法用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")