У меня есть следующий код:
from z3 import *
a0 = Int('a0')
a1 = Int('a1')
a2 = Int('a2')
v1 = BitVec('v1',32)
s.add(v1 == ((a0 + a1) >> 31) >> 30)
s.add(((v1 + a2) & 3) - v1 == 1)
Теперь я получаю следующую ошибку:
TypeError: unsupported operand type(s) for >>: 'ArithRef' and 'int'
Я понимаю проблему, z3 не может обработать подразумеваемое преобразование как нативноеПитон может (то есть 45 >> 3 напрямую преобразуется в 5).Однако мне нужно, чтобы мои переменные a_i были Ints.Есть ли способ добиться этого?