<p><span class="h-card" translate="no"><a href="https://mastodon.social/@regehr" class="u-url mention">@<span>regehr</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> oh, this is really good to know, because my input space can be easily hundreds of bits and in the most general case any subset of them can be undef</p><p>i wonder if i should not feed the entire netlist to the solver but rather extract just the little bits my rewriting engine modifies (by doing RAUW) and then seeing if i can trace both the original and the new instruction for each RAUW to a common subset of bits...</p>