Z3py: решение с целыми числами и битовыми векторами в ограничениях

Я пытаюсь решить ограничения с помощью решателя Z3 SMT в python. Ограничения включают как целые числа, так и битовые векторы. Я конвертирую BitVec в Int с помощью Z3_mk_bv2int. Я считаю, что следующие ограничения невыполнимы, но я получаю тест SAT от решателя Z3. Не уверен, правильно конвертирую или нет. Однако, если я заменю переменные BitVecs ограниченными целочисленными переменными, преобразование не потребуется, и я получу ожидаемые результаты.

Пример:

def get_int(var):

ctx = var.ctx

    return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), ctx)

def main():

    var1 = BitVec('var1', 6)
    var2 = Int('var2')
    solve(var2 == get_int(var1)- var2, var2 > 32)

if __name__ == "__main__": main()

Результаты: [var1 = 0, var2 = 33]

Я новичок в решателях SMT. Пожалуйста, помогите мне разобраться в ошибке или найти альтернативное решение.