Использование Z3Py с Python 3.3

Моя ситуация

Я установил Microsoft Z3 (Z3 [version 4.3.0 - 64 bit]. (C) 2006) и pyc исполняемых файлов для Python2.

Я написал пакет Python3, которому нужен доступ к функциям z3.

Чтобы иметь возможность использовать pyc двоичные файлы с моим пакетом Python3, я decompyle z3 двоичных файлов применил 2to3.

Моя проблема

Int('string') не работает, потому что Z3Py не может обрабатывать новый <class 'str'>, используемый в качестве аргумента 'string':

>>> import z3; z3.Int('abc')

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File ".\bin\z3.py", line 2931, in Int
    return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
  File ".\bin\z3.py", line 72, in to_symbol
    return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
  File ".\bin\z3core.py", line 1430, in Z3_mk_string_symbol
    r = lib().Z3_mk_string_symbol(a0, a1)
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type

Мои вопросы

• Немного хакерски нужно сначала decompyle *.pyc файлов Z3. Итак, есть ли исходные коды Z3Py?
• Существует ли уже существующий порт Z3Py на Python3?
• Любая другая идея, как заставить Z3Py работать с Python3?

Спасибо. - Если что-то непонятно, пожалуйста, оставьте вопрос в комментарии.