<p>&quot;use an SMT solver&quot;, they said. &quot;it will be fun&quot;, they said</p><p>(the total amount of bytes is 32)</p>