<p><span class="h-card" translate="no"><a href="https://mastodon.social/@whitequark" class="u-url mention">@<span>whitequark</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@lenary" class="u-url mention">@<span>lenary</span></a></span> <span class="h-card" translate="no"><a href="https://hachyderm.io/@unlambda" class="u-url mention">@<span>unlambda</span></a></span> inputs can be partially undef. so, like, we might get all odd numbers or something. this means that the input space for a 64 bit variable isn't 2^64 but rather 2^2^64. the resulting queries are effectively impossible to solve without good quantifier elimination, which Z3 doesn't seem to have.</p><p>in this case, Alive2 simply cuts a corner, it does not reason about the full 2^2^N, or nothing would ever get solved. this doesn't seem to matter much in practice.</p>
