按位與Z3？

Question

我寫了下面的Z3 Python代碼

x, y = Ints('x y') 
F = (x == y & 16)  # x has the value of (y & 16) 
print F 

，但我得到波紋管錯誤：

TypeError: unsupported operand type(s) for &: 'instance' and 'int' 

怎麼辦按位運算（&在這種情況下）在Z3方程？

謝謝。

Answer 1

x和y應該是位向量：

x, y = BitVecs('x y', 32) 
F = (x == y & 16)  # x has the value of (y & 16) 
print F 

見Bitvectors部分下http://rise4fun.com/Z3/tutorial/guide