Uncaught exception thrown of type AssertionError

[ZhuXiaoran07]

When kompiling the following definition:

module TEST-SYNTAX 
  syntax Stmt  ::= "COUNTER" "=" Id ";"   
endmodule
module TEST
  imports TEST-SYNTAX
  syntax KResult ::= Int | Bool | String
  configuration <T color="yellow">
                    <k> $PGM:Stmt</k>
                  <counters>
                  <counter multiplicity="*"> .K </counter>
                  </counters> 
                </T>

    rule <k> COUNTER=I; =>. ...</k>
         <counters> CT:Bag(.Bag =><counter> I </counter>) </counters> 
endmodule

it results in [Error] Internal: Uncaught exception thrown of type AssertionError. Please rerun your program with the --debug flag to generate a stack trace, and file a bug report at https://github.com/kframework/k/issues.

But if modify the counters cell in the rule as following:

module TEST-SYNTAX 
  syntax Stmt  ::= "COUNTER" "=" Id ";"   
endmodule
module TEST
  imports TEST-SYNTAX
  syntax KResult ::= Int | Bool | String
  configuration <T color="yellow">
                    <k> $PGM:Stmt</k>
                  <counters>
                  <counter multiplicity="*"> .K </counter>
                  </counters> 
                </T>

    rule <k> COUNTER=I; =>. ...</k>
         <counters> CT:Bag =>CT (<counter> I </counter>) </counters>
endmodule

works well when being kompiled.

┆Issue is synchronized with this Asana task

[cos]

it looks like a bug in concretization. thanks for submitting!