Variable name appears twice with different sorts

[virgil-serbanuta]

kore-exec dump: kore-exec.tar.gz

To reproduce using the k sources:

Use this branch: https://github.com/virgil-serbanuta/verified-smart-contracts/tree/multisig.bug5/multisig/protocol-correctness/proof Command line:

cd multisig/protocol-correctness/proof
make execution.timestamp && kprove proof-perform-remove-user-1.k

The error looks like this:

kore-exec: [51947972] Error (ErrorException):
    while normalizing substitution
        normalized:
            variable:
                RuleVarV:SortKItem{}
            term:
                /* Fl Fn D Sfc */
                /* Inj: */ inj{SortExpressionList{}, SortKItem{}}(
                    /* Fl Fn D Sfa */ RuleVarV:SortExpressionList{}
                )
        denormalized:

    while wrapping substitution
        assigned variable: RuleVarV:SortKItem{}
        assigned term:
            /* Fl Fn D Sfc */
            /* Inj: */ inj{SortExpressionList{}, SortKItem{}}(
                /* Fl Fn D Sfa */ RuleVarV:SortExpressionList{}
            )
    Assertion failed
    CallStack (from HasCallStack):
      assert, called at src/Kore/Internal/Substitution.hs:429:11 in kore-0.40.0.0-DshaysOjWTvItB8JRMIn4C:Kore.Internal.Substitution
      unsafeWrap, called at src/Kore/Internal/Substitution.hs:450:5 in kore-0.40.0.0-DshaysOjWTvItB8JRMIn4C:Kore.Internal.Substitution
      unsafeWrapFromAssignments, called at src/Kore/Internal/Condition.hs:183:11 in kore-0.40.0.0-DshaysOjWTvItB8JRMIn4C:Kore.Internal.Condition
      fromNormalizationSimplified, called at src/Kore/Step/Simplification/SubstitutionSimplifier.hs:137:29 in kore-0.40.0.0-DshaysOjWTvItB8JRMIn4C:Kore.Step.Simplification.SubstitutionSimplifier

[ttuegel]

We should never see RuleVarV:SortKItem{} and RuleVarV:SortExpressionList{}, so I'm extremely suspicious of what the frontend is passing us. But, I'm not able to find anything wrong with the Kore definition.