Booster reports `Stuck` but should branch or abort

[jberthold]

The following test file reproduces a situation where booster returns a stuck result but should instead either branch or abort on the given input. When using default settings, the kore-rpc-booster app falls back to kore in this case, which correctly constructs the branches.

test.k

module TEST
  imports K-EQUAL

  syntax State ::= "A" [symbol(A)]
                 | "B" [symbol(B)]
                 | "C" [symbol(C)]
                 | "D" [symbol(D)]

  configuration <k> $PGM:State </k>

  rule <k> A ~> B => A ... </k>
  rule <k> A ~> C => C ... </k>
  rule <k>    D   => A ~> ?UNKNOWN:State ... </k>
    ensures ?UNKNOWN =/=K D

endmodule

On input A ~> UNKNOWN:State ~> .K, the rewrite should branch based on what UNKNOWN is:

• UNKNOWN == B => result A ~> .K
• UNKNOWN ==C => Result C ~> .K
• otherwise stuck with A ~> UNKNOWN ~> .K (A ~> A ~> .K or A ~> D ~> .K)

This is a bug in the rewrite code, introduced in #3820. The SubjectVariableMatch failure must lead to aborting the rewrite.