我想用 z3 來解決這個案例。輸入是一個 10 個字符的字符串。輸入的每個字符都是一個可打印字符 (ASCII)。輸入應(yīng)該是這樣的，當(dāng)使用輸入作為參數(shù)調(diào)用 calc2() 函數(shù)時，結(jié)果應(yīng)該是：0x0009E38E1FB7629B。在這種情況下如何使用 z3py？通常我只會添加獨立方程作為對 z3 的約束。在這種情況下，我不確定如何使用 z3。def calc2(input):    result = 0    for i in range(len(input)):        r1 = (result << 0x5) & 0xffffffffffffffff        r2 = result >> 0x1b        r3 = (r1 ^ r2)        result = (r3 ^ ord(input[i]))    return resultif __name__ == "__main__":        input = sys.argv[1]        result = calc2(input)        if result == 0x0009E38E1FB7629B:             print "solved"更新：我嘗試了以下操作，但是它沒有給我正確的答案：from z3 import *def calc2(input):    result = 0    for i in range(len(input)):        r1 = (result << 0x5) & 0xffffffffffffffff        r2 = result >> 0x1b        r3 = (r1 ^ r2)        result = r3 ^ Concat(BitVec(0, 56), input[i])    return resultif __name__ == "__main__":    s = Solver()    X = [BitVec('x' + str(i), 8) for i in range(10)]    s.add(calc2(X) == 0x0009E38E1FB7629B)    if s.check() == sat:        print(s.model())