title: z3py error when converting int to bitvec
body: <p>From (<a href="https://stackoverflow.com/questions/16476658/z3-is-it-possible-to-sum-up-a-bitvec-and-a-real">Z3: Is it possible to sum up a BitVec and a Real?</a>) , I tried to convert an int to bitvec using</p>
  
  <pre><code>x = Int('x')
  reg = BitVecRef(Z3_mk_int2bv(BitVecVal(x.ctx_ref(), 16, x)), x.ctx)
  </code></pre>
  
  <p>but I always get an error saying " 'Ast' object has no attribute 'ref' ", it seems this function can only convert integer to bitvec, is there any other way to convert Int to bitvec? </p>
  
  <p>Also I know this function is treated as uninterpreted for now, do I need to recompile my local version from (<a href="https://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option">bv-enable-int2bv-propagation option</a>) ?</p>
  
  <p>Thanks in advance!</p>