Rewriting multiple items in a KSequence causes a crash #2023
Description
module TEST
imports INT
configuration <k> foo ~> 1 ~> 2 ~> 3 ~> 4</k>
syntax KItem ::= "foo" | "bar"
rule <k> (foo ~> X ~> Y) => (X ~> bar) ... </k>
endmodule
crashes with kore-exec.tar.gz
kore-exec: [230272] Error (ErrorRewritesInstantiation):
While rewriting the configuration:
\and{SortGeneratedTopCell{}}(
/* term: */
/* Fl Fn D Sfa Cl */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fl Fn D Sfa Cl */
Lbl'-LT-'k'-GT-'{}(
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cl */ Lblfoo'Unds'TEST'Unds'KItem{}(),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("1")
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("2")
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("3")
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("4")
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
)
)
),
/* Fl Fn D Sfa Cl */
Lbl'-LT-'generatedCounter'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
)
),
\and{SortGeneratedTopCell{}}(
/* predicate: */
/* D Sfa */ \top{SortGeneratedTopCell{}}(),
/* substitution: */
\top{SortGeneratedTopCell{}}()
))
Unable to instantiate semantic rule at /home/njr/co/github.com/nishantjr/boogie-semantics/./test.k:5:10-5:52
Unification did not find a solution for the variables:
RuleVar'Unds'DotVar1 RuleVarX RuleVarY
The unification solution was:
\and{SortGeneratedTopCell{}}(
/* term: */
/* Spa */
\rewrites{SortGeneratedTopCell{}}(
/* Spa */
\and{SortGeneratedTopCell{}}(
/* D Sfa */ \top{SortGeneratedTopCell{}}(),
/* Fn Sfa */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fn Sfa */
Lbl'-LT-'k'-GT-'{}(
/* Fn Sfa */
kseq{}(
/* Fl Fn D Sfa Cl */
Lblfoo'Unds'TEST'Unds'KItem{}(),
/* Fn Sfa */
append{}(
/* Fl Fn D Sfa */ RuleVarX:SortK{},
/* Fn Sfa */
append{}(
/* Fl Fn D Sfa */ RuleVarY:SortK{},
/* Fl Fn D Sfa */
RuleVar'Unds'DotVar1:SortK{}
)
)
)
),
/* Fl Fn D Sfa */
RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}
)
),
/* Fn Spa */
Lbl'-LT-'generatedTop'-GT-'{}(
/* Fn Spa */
Lbl'-LT-'k'-GT-'{}(
/* Fn Spa */
append{}(
/* Fl Fn D Sfa */ RuleVarX:SortK{},
/* Fl Fn D Spa */
kseq{}(
/* Fl Fn D Sfa Cl */
Lblbar'Unds'TEST'Unds'KItem{}(),
/* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
)
)
),
/* Fl Fn D Sfa */
RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}
)
),
\and{SortGeneratedTopCell{}}(
/* predicate: */
/* Sfa */
\equals{SortK{}, SortGeneratedTopCell{}}(
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1")
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("2")
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("3")
),
/* Fl Fn D Sfa Cl */
kseq{}(
/* Fl Fn D Sfa Cli */
/* Inj: */ inj{SortInt{}, SortKItem{}}(
/* Fl Fn D Sfa Cl */
/* builtin: */ \dv{SortInt{}}("4")
),
/* Fl Fn D Sfa Cl */ dotk{}()
)
)
)
),
/* Fn Sfa */
append{}(
/* Fl Fn D Sfa */ RuleVarX:SortK{},
/* Fn Sfa */
append{}(
/* Fl Fn D Sfa */ RuleVarY:SortK{},
/* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
)
)
),
/* substitution: */
/* Spa */
\equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}(
/* Fl Fn D Sfa */ RuleVar'Unds'DotVar0:SortGeneratedCounterCell{},
/* Fl Fn D Sfa Cl */
Lbl'-LT-'generatedCounter'-GT-'{}(
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
)
)
))
Error! Please report this.
CallStack (from HasCallStack):
checkSubstitutionCoverage, called at src/Kore/Step/RewriteStep.hs:139:9 in kore-0.26.0.0-AoemVAjaFzZKWETfKV1QVF:Kore.Step.RewriteStep