title: Z3 int2bv operation
body: <p>I am experiencing some issues with the bitvector operations. In particular, given the following model. I was expecting <code>var0</code> to be <code>11</code>. </p>
  
  <pre><code>(declare-const var1 Int)
  (declare-const var0 Int)
  (assert (= var1 10))
  (assert (= var0 ((_ bv2int 32) (bvor ((_ int2bv 32) var1) ((_ int2bv 32) 1)))))
  (check-sat)
  (get-model)
  (exit)
  </code></pre>
  
  <p>However, the solution given by Z3 for fun was:</p>
  
  <pre><code>sat (model 
  (define-fun var1 () Int 10) 
  (define-fun var0 () Int (- 1)) 
  )
  </code></pre>
  
  <p>This means, -1 instead of 10. Am I doing something wrong?</p>