title: Bit-wise with Z3?
body: <p>I write the following Z3 python code</p>
  
  <pre><code>x, y = Ints('x y')
  F = (x == y &amp; 16)      # x has the value of (y &amp; 16)
  print F
  </code></pre>
  
  <p>But I get bellow error:</p>
  
  <pre><code>TypeError: unsupported operand type(s) for &amp;: 'instance' and 'int'
  </code></pre>
  
  <p>How to do bitwise arithmetic (&amp; in this case) in Z3 equation? </p>
  
  <p>Thanks.</p>