Open virgil-serbanuta opened 1 year ago
Is this another problem with the type inferencer, @radumereuta? It complains Sort variable Q10 not declared.
, but the generated rule has the attribute sortParams({Q10})
The kore term that gets generated:
\equals{SortBool{},SortGeneratedTopCell{}}(
\and{SortBool{}}( \dv{SortBool{}}("true"), \equals{Q10, SortBool{}}(
\equals{SortInt{}, Q10}(
\dv{SortInt{}}("0"),
Lbl'Hash'bool'LParUndsRParUnds'A'Unds'Int'Unds'Bool{}(VarB:SortBool{})
),
\equals{SortBool{}, Q10}(
\dv{SortBool{}}("false"),
VarB:SortBool{}
)
)
),
\dv{SortBool{}}("true")
)
Ah, I missed this issue. Thank you for adding it to the board. @virgil-serbanuta can you please add the issues you post in the K repo to the K Development board? Just to make sure we don't miss it.
@gtrepta I'm not sure. It might be an issue with ModuleToKore. This needs more investigation.
Try to fix the generated file and see if it passes. Then we can see if we can fix it when it's being generated.
I tried changing Q10
to SortK{}
and kore-exec stopped complaining about it. I wasn't able to get a full run of it though because the example produced in kore-exec.tar.gz
doesn't have an argument for --pattern
which kore-exec requires.
Check again when we make more progress on: https://github.com/runtimeverification/k/issues/3601
What component is the issue in?
Front-End
Which command
What K Version?
v6.0.57-0-ga91e8fd25a-dirty
Operating System
Linux
K Definitions (If Possible)
Steps to Reproduce
Expected Results
The source above should just compile. If that's unfeasible,
#Iff
should be available (it does not show up inkast.md
).