<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> </p><p>so the best reference here is the Alive2 paper where we describe the refinement check in a lot of detail.</p><p>but let me take a stab...</p><p>an equivalence check is easy: you ask the solver whether there exists a valuation of the inputs that makes source and target behave differently.</p><p>then, the refinement check is basically asking the solver whether there exist inputs that cause target to have a behavior not seen in source. target can have fewer behaviors but not more.</p>