Buggy decision tree generated in case involving overloads

I have another example of the llvm backend generating broken decision trees. It's quite remarkable that I've managed to uncover so many of these issues that have gone undetected for so long.

Here is the K definition which reproduces the error:

module TEST-COMMON
  syntax ConstructorName [token]
  syntax Name [token]

  syntax Exp ::= Name
  syntax Exp ::= Val
  syntax Val ::= Name
  syntax Exps  ::= List{Exp,","}                   [klabel(exps)]
  syntax Vals ::= List{Val,","}                    [klabel(exps)]
  syntax Names ::= List{Name,","}                  [klabel(exps)]
  syntax Exps ::= Names
  syntax Exps ::= Vals
  syntax Vals ::= Names
  syntax Exp ::= ConstructorName "(" Exps ")"      [klabel(constructor)]
  syntax Val ::= ConstructorName "(" Vals ")"      [klabel(constructor)]
endmodule

module TEST-SYNTAX
  imports TEST-COMMON
  syntax ConstructorName ::= r"[A-Za-z]+" [token]
  syntax Name ::= ConstructorName [token]
endmodule

module TEST
  imports TEST-COMMON
  syntax Names ::= getNames(Exp) [function]
  rule getNames(C:ConstructorName(E:Exp,Es:Exps)) => getNames(E)
  rule getNames(N:Name) => N

  rule (E::Exp => getNames(E):KItem)
endmodule

The program that reproduces the error is Pair(m,n). What happens is that the occurrence used to get the value bound to the variable E in the first rule for getNames is incorrectly bound, and thus it reads an undefined value when the value on the stack is loaded to be passed to the function that constructs the right hand side. this leads to an incorrect term representation that either segfaults or simply gets stuck. The correct output of this program ought to be m.

I'm not entirely sure exactly what is going wrong with the decision tree generation process yet. It appears to be related to the case where we make use of MakePattern nodes to construct an injection which is not actually part of the term being matched. This has something to do with the overloaded productions, in particular, it appears due to the conjunction of the overload on exps and the overload on constructor. Somehow the case when you match on a Val that contains a Names leads it to use the wrong occurrence when constructing the pattern which is passed to the leaf node. I know what the correct occurrence ought to be, but I still need to reason through exactly where the current algorithm is going wrong.

runtimeverification / llvm-backend

Buggy decision tree generated in case involving overloads #676