Invalid axioms generated (asserting \bottom{S} unconditionally)

[jberthold]

The K-compiler currently generates invalid axioms like axiom{} \bottom{S}() [constructor{}()] // no junk (for S in SortSet, SortMap, SortList, and SortK).
These axioms state that \bottom is \top and could be used to prove anything we want (the Haskell back-end skips these invalid axioms at the moment).

To reproduce:

$ echo "module TEST endmodule" > test.k
$ kompile test.k
$ grep -e "axiom.. .bottom" test-kompiled/definition.kore
  axiom{} \bottom{SortList{}}() [constructor{}()] // no junk
  axiom{} \bottom{SortK{}}() [constructor{}()] // no junk
  axiom{} \bottom{SortMap{}}() [constructor{}()] // no junk
  axiom{} \bottom{SortSet{}}() [constructor{}()] // no junk

[ehildenb]

Here, if the list is empty, the axiom should not be emitted: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java#L777

[Robertorosmaninho]

Hey @jberthold, the expected behavior doesn't have any axioms in this case, right? E.g., delete these lines that have axioms for empty collections.

[jberthold]

Correct, these axioms should just not be there.