APR-unsound behaviour when rule RHS definedness cannot be established

In discussion with @virgil-serbanuta, I have understood that when applying rules whose RHS contains partial functions, the behaviour of the backend should roughly amount to the following:

1. Branch on #Ceil(RHS)
2. In the branch with #Ceil(RHS), apply the rule and continue
3. In the branch with #Not (#Ceil (RHS)), do not apply the rule

which amounts to implicitly having #Ceil(RHS) as a requires. Normally, the #Not (#Ceil (RHS)) branch can be trivially discarded, and cases in which it cannot indicate a problem with how the semantics is defined.

Currently, the behaviour is:

1. Apply the rule
2. Branch on definedness

This leads to configurations in which both a term and the fact that this term is not defined are present, leading to legitimate branches being discarded as vacuous and therefore breaking all-path-reachability.

This was revealed by this PR (before commit a35b70e, in which pyk was made to check subsumption into the target nodes only in the case of terminal nodes if the target is terminal. This broke this test, which used this rule

    rule <k> ECREC => #end EVMC_SUCCESS ... </k>
         <callData> DATA </callData>
         <output> _ => #ecrec(#range(DATA, 0, 32), #range(DATA, 32, 32), #range(DATA, 64, 32), #range(DATA, 96, 32)) </output>

and treated the branch in which the above #ecrec was both present in the <output> cell and declared as not defined (via #Not (#Ceil ( ... ))).

Start with tests/specs/benchmarks/ecrecover00-siginvalid-spec.k and the behavior change described around PR 1996, including commit a35b70e. Trace how the backend handles rule application and definedness for the shown #ecrec RHS; done means the invalid branch is excluded before it produces a configuration containing both the term and its negated definedness, while the test passes.