title: Z3 - How to set a byte constraint on a BitVec
body: <p>I'm trying to set a list of possible allowed bytes in a BitVec but I'm not sure I'm actually setting the constraints in the right way.</p>
  
  <p>E.g:</p>
  
  <p>Let us have a 32 bit BV called <code>bv</code> and a <code>Solver()</code> called <code>s</code>:</p>
  
  <pre><code>s = Solver()
  bv = BitVec(8 * 4)
  </code></pre>
  
  <p>I want that each byte can be either <code>0x2</code> or <code>0x34</code> or <code>0xFF</code> so I used <code>Extract()</code>:</p>
  
  <pre><code>i = 0
  while (i &lt; 8 * 4):
      s.add(Extract(i + 7, i, bv) == 0x2)
      s.add(Extract(i + 7, i, bv) == 0x34)
      s.add(Extract(i + 7, i, bv) == 0xFF) 
      i += 8
  </code></pre>
  
  <p>Sadly, <code>s.check()</code> returns <code>unsat</code>. </p>
  
  <p>I think this is not the correct way to express that those bytes <strong>may be <em>0x2 OR 0x34 OR 0xFF</em></strong>.
  Did I write the constraints in the right way or my thought process is just plain wrong?</p>