title: Z3 sort conversion: (one character) String to (length 8) bitvector
body: <p>Referring to a previously asked SO question about <a href="https://stackoverflow.com/questions/46522705/extracting-decimal-value-from-a-character-in-a-z3-string">extracting the decimal value from a Z3 string</a>, I know that <strong>converting a BitVec8 to a one character string is possible</strong>. For example, running this query:</p>
  
  <pre><code>(declare-const s String)
  (declare-const someBV8 (_ BitVec 8))
  (assert (= (str.len s) 6))
  
  (assert (= someBV8 #x62))
  (assert (= (seq.unit someBV8) (str.at s 2)))
  (assert (= (seq.unit someBV8) (str.at s 3)))
  (assert (= (seq.unit someBV8) (str.at s 4)))
  
  (check-sat)
  (get-value (s))
  </code></pre>
  
  <p>gives the following output:</p>
  
  <pre><code>sat
  ((s "\x00\x00bbb\x00"))
  </code></pre>
  
  <p>I wanted to know if the opposite conversion exists too? <strong>Is it possible to convert a one character string to a BitVec8?</strong> Something like str2bv:</p>
  
  <pre><code>(declare-const s String)
  (declare-const someBV8 (_ BitVec 8))
  (assert (= (str.len s) 6))
  
  (assert (= someBV8 #x62))
  (assert (= someBV8 (str2bv (str.at s 2))))
  (assert (= someBV8 (str2bv (str.at s 3))))
  (assert (= someBV8 (str2bv (str.at s 4))))
  
  (check-sat)
  (get-value (s))
  </code></pre>