Cannot apply rule for symbolic list with multiple elements

[virgil-serbanuta]

Symbolic list unification fails with multiple elements

To reproduce:

tmp.k:

module TMP
  imports INT
  imports LIST

  syntax KItem ::= "push" | "pop"
  syntax KItem ::= Int

  rule  <k> push => .K ... </k>
        <stack> (.List => ListItem(1)) ... </stack>

  rule  <k> pop => .K ... </k>
        <stack> (ListItem(_:KItem) => .List) ... </stack>
    [label(xyzzy)]

  configuration
    <T>
      <k color="green"> .K </k>
      <stack> .List </stack>
    </T>

endmodule

tmp-proof.k:

module TMP-PROOF
  imports TMP

  claim 
      <T>
        <k> push ~> push ~> pop ~> pop ~> K:K </k>
        <stack> Stack:List </stack>
      </T>
      =>
      <T>
        <k> K </k>
        <stack> Stack </stack>
      </T>
endmodule

to run:

kompile tmp.k --backend haskell && kprove tmp-proof.k

The repl provides no reason explaining why the xyzzy rule is not applied:

Kore (0)> step 2
Kore (2)> try xyzzy
No explanation given
Kore (2)> 

Note that the claim above works with a single push/pop, i.e. <k> push ~> pop ~> K:K </k>

[ttuegel]

This is a known limitation.

[Sereja313]

@ana-pantilie I managed to reproduce this error.
backend version:

Kore version 0.60.0.0
Git:
  revision:	74bc7a963a825d0f0f034b5d3412dc59448e51bb (dirty)
  branch:	master
  last commit:	Tue Feb 7 05:02:49 2023 -0700