title: Bad performance when using `str.indexof` with `int2bv`
body: <p>I am trying to constrain a bitvector to be equal to the index of a null byte in a string. However, I am getting performance issues with <code>int2bv</code>. </p>
  
  <p>As a simple example of the issue, this problem (without <code>int2bv</code>) solves instantly:</p>
  
  <pre><code>; Solve time: 0m0.065s
  (declare-const s String)
  (declare-const len Int)
  (assert (= (str.indexof s "\00") len))
  (assert (&gt;= len 256)) ; 0x100
  (assert (&lt;= len 4095)) ; 0xFFF
  (check-sat)
  (get-model)
  </code></pre>
  
  <p>On the other hand, the "same" problem (it allows strictly more solutions) using <code>int2bv</code> takes almost 2 minutes:</p>
  
  <pre><code>; Solve time: 1m54.861s
  (declare-const s String)
  (declare-const len Int)
  (assert (= (str.indexof s "\00") len))
  (assert (&gt;= len 0))
  (assert (not (= (bvand ((_ int2bv 12) len) #xF00) #x000)))
  (check-sat)
  (get-model)
  </code></pre>
  
  <p>Is there a better way to encode this kind of bitvector string length operation in z3? <a href="http://smt-workshop.cs.uiowa.edu/2016/slides/berzish.pdf" rel="nofollow noreferrer">These slides</a> on z3strBV claim to have better support, but their extensions don't seem to be implemented in the standard z3 distribution.</p>
  
  <p>I am using z3 version 4.8.0 - 64 bit and running with <code>smt.string_solver=z3str3</code>.</p>