title: Why does Z3 say that this equation is not satisfiable, when I have input that is correct?
body: <p>Given a simple shift-and-XOR operation, where 'input' is symbolic:</p>
  
  <pre><code>input    = BitVec('input',32)
  feedback = 0x8049d30
  shiftreg = input ^ feedback
  shiftreg = 0xffffffff &amp; ((shiftreg &lt;&lt; 8) | (shiftreg &gt;&gt; 24))
  shiftreg = shiftreg ^ 0xcafebabe
  
  s = Solver()
  s.add(shiftreg == 0x804a008)
  s.check()
  # unsat
  </code></pre>
  
  <p>We are told that this equation is not solvable.  If printed, <code>s</code> contains:</p>
  
  <pre><code>[4294967295 &amp;
   ((input ^ 134520112) &lt;&lt; 8 | (input ^ 134520112) &gt;&gt; 24) ^
   3405691582 ==
   134520840]
  </code></pre>
  
  <p>However, I can trivially create an example that solves this equation for 'input'.</p>
  
  <pre><code>want = 0x804a008
  want ^= 0xcafebabe
  want = 0xffffffff &amp; ((want &gt;&gt; 8) | (want &lt;&lt; 24))
  want ^= 0x8049d30
  print hex(want)
  # 0xbec6672a
  </code></pre>
  
  <p>Entering our solution into Z3's equation, we see that we can satisfy it.</p>
  
  <pre><code>input = 0xbec6672a
  [4294967295 &amp;
   ((input ^ 134520112) &lt;&lt; 8 | (input ^ 134520112) &gt;&gt; 24) ^
   3405691582 ==
   134520840]
  # True
  </code></pre>
  
  <p>Why can Z3 not find this solution?</p>