CODEWITHSUNDEEP
pythonz3z3py
S. L.
S. L.

Reputation: 680

Z3 bitvecs to Int and back

I have the following code:

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)

Now I'm getting the following error:

TypeError: unsupported operand type(s) for >>: 'ArithRef' and 'int'

I understand the problem, z3 can't handle implied conversion like native python can (i.e. 45 >> 3 is directly converted to 5). However, I need my variables a_i to be Ints. Is there a way to achieve this?

Upvotes: 1

Views: 6869

Answers (1)

alias
alias

Reputation: 30428

You're looking for BV2Int and Int2BV. See here:

https://z3prover.github.io/api/html/namespacez3py.html#a7954eb7ea27b3972070ac9eb6f5946a2

https://z3prover.github.io/api/html/namespacez3py.html#ac516cd29fb1da802c07a51b6be605115

Upvotes: 4

Related Questions