Решите несколько уравнений, используя Z3

У меня есть следующая функция, которая принимает входную строку и число для создания хэша, как показано ниже:

#! /usr/bin/python

def calc_hash(key, num):
    result = 0

    for i in range(len(key)):
        result = (ord(key[i]) + result * 10 - 0x30) % num

    return result

if __name__ == "__main__":
    print hex(calc_hash("you_must_check_this_out", 0x1A5D215))

Итак, если входная строка: «you_must_check_this_out», а число: 0x1A5D215, то вывод будет: 0x7cda66.

Цель состоит в том, чтобы найти входную строку, удовлетворяющую следующим условиям:

calc_hash(input, 0x1A5D215) == 0xd5
calc_hash(input, 0x28DB) == 0xe5
calc_hash(input, 0x5d1) == 0x19
calc_hash(input, 0xff7ff) == 0x53
calc_hash(input, 0x3eff) == 0x87

Я не знаю длину входной строки, однако ограничение на длину заключается в том, что она должна быть меньше или равна 30.

len(input) <= 30

Итак, я написал следующий код, чтобы найти решение с помощью Z3, однако он не работает.

#! /usr/bin/python

import sys
from z3 import *

def calc_hash(input, num):
    result = 0

    for i in range(len(input)):
        result = (ZeroExt(56, input[i]) + result * 10 - 0x30) % num

    return result

if __name__ == "__main__":
    s = Solver()

    input = [BitVec("input%s" % i, 8) for i in range(10)]

    for i in range(10):
      s.add(input[i] >= 0x20)
      s.add(input[i] <= 0x7E)

    s.add(calc_hash(input,0x1A5D215) == 0xd5)
    s.add(calc_hash(input,0x28DB) == 0xe5)
    s.add(calc_hash(input,0x5d1) == 0x19)
    s.add(calc_hash(input,0xff7ff) == 0x53)
    s.add(calc_hash(input,0x3eff) == 0x87)

    print s.check()

    print s.model()

Длина ввода может быть изменена в коде, чтобы попробовать разные длины.

Есть ли проблема с приведенным выше кодом?