在 Z3 Python 中，要提取 BitVector V 的 8 位，我们可以执行以下操作：
Extract(7, 0, V)
但是，有时在我的程序中，V 可以是一个常数，所以在这种情况下，代码实际上是这样的：
Extract(7, 0, 0x87654)
不幸的是，这是错误的，因为上面的代码没有指定 0x87654 是 32 位 BitVector.7
一种解决方案是创建一个临时变量，例如：
tmp = BitVec('tmp', 32)
tmp == 0x87654
Extract(7, 0, tmp)
但是，这有点麻烦，因为我必须创建一个临时的才能工作。我想知道是否有另一种方法而不必创建临时变量？有没有办法在我的代码中将 0x87654 转换为 BitVector 内联？
非常感谢。