title: Z3: Translate a BoolRef into a BitVecVal
body: <p>I am trying to simulate the <code>x86</code> assembly code using <code>z3</code> formulas. Currently, I am trapped in simulating the semantics of <code>setnz</code> opcode.</p>
  
  <p>the semantics of <code>setnz</code> is defined as </p>
  
  <pre><code>checking the value of CPU flag `ZF`, and if it is equal to 1, then set a register byte as 1, otherwise set it as 0.
  </code></pre>
  
  <p>For example, the above procedure can be simulated in this way:</p>
  
  <pre><code>python
  &gt;&gt;&gt; from z3 import *
  &gt;&gt;&gt; a = BitVecVal(1, 1)
  &gt;&gt;&gt; c = (a == 1)
  &gt;&gt;&gt; set_register("al", c)
  </code></pre>
  
  <p>However, <strong>note that the type of <code>c</code> is a <code>BoolRef</code>, and I would like to set the value of <code>al</code> as a 8-bit long <code>BitVecVal</code>.</strong></p>
  
  <p>So here is my question:</p>
  
  <ol>
  <li>I am following the best practice to simulate such <code>set</code> opcodes?</li>
  <li>If so, how can I translate a <code>BoolRef</code> into a 8-bit long <code>BitVecVal</code> in order to set the register?</li>
  </ol>