title: Z3 bitvecs to Int and back
body: <p>I have the following code:</p>
  
  <pre><code>from z3 import *
  
  a0 = Int('a0')
  a1 = Int('a1')
  a2 = Int('a2')
  v1 = BitVec('v1',32)
  
  s.add(v1 ==  ((a0 + a1) &gt;&gt; 31) &gt;&gt; 30)
  s.add(((v1 + a2) &amp; 3) - v1 == 1)
  </code></pre>
  
  <p>Now I'm getting the following error:</p>
  
  <pre><code>TypeError: unsupported operand type(s) for &gt;&gt;: 'ArithRef' and 'int'
  </code></pre>
  
  <p>I understand the problem, z3 can't handle implied conversion like native python can (i.e. <code>45 &gt;&gt; 3</code> is directly converted to <code>5</code>). However, I need my variables <code>a_i</code> to be Ints. Is there a way to achieve this?</p>