Feature: custom unification rules

I've attempted to add the following rule to a KEVM proof:

    rule [fast-unification-failure]: { <kevm> <k> K_CELL </k> ... </kevm> #Equals <kevm> <k> K_CELL' </k> ... </kevm> } => #Bottom requires K_CELL =/=K K_CELL' [simplification(20)]

I can see in definition.kore (bug report attached storagevar00-spec.tar.gz), that the rule makes it into the backend. I've also marked several other rules with labels. I'm calling the backend with export KORE_EXEC_OPTS="--debug-equation VERIFICATION.fast-unification-failure --debug-equation VERIFICATION.test1 --debug-equation VERIFICATION.test2 --debug-equation VERIFICATION.test3 --bug-report tests/specs/benchmarks/storagevar00-spec --log tests/specs/benchmarks/storagevar00-spec.debug-log --log-format oneline --log-entries DebugTransition,DebugAttemptedRewriteRules", so that we can see attempts of these equations.

In the debug log (attached storagevar00-spec.debug-log.txt), I can see that equation test1 in exercised, but simplification rule fast-unification-failure never is. I use command grep 'DebugAttemptEquation' tests/specs/benchmarks/storagevar00-spec.debug-log | cut -d ':' -f3-4 | sort -u to see this.

Can the Haskell backend try user-supplied unification rules before trying the default unification algorithm when applying semantic rules? Maybe if they are simplification(N) for N < 50 rules, or N < 25?

Start with the attached definition.kore and storagevar00-spec.debug-log.txt, then reproduce the command using tests/specs/benchmarks/storagevar00-spec and inspect the DebugAttemptEquation entries for test1 and fast-unification-failure. Determine how user-supplied unification rules should be prioritized relative to the default algorithm, including the simplification threshold. Done means the backend attempts the requested custom rule when applying semantic rules.