search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
444 stars 147 forks source link

Remove old workaround #4485

Closed Baltoli closed 3 months ago

Baltoli commented 3 months ago

In https://github.com/runtimeverification/k/commit/7ba37fb32f357b0deee710a83b6e58501a2b7212 (8 years ago), we disabled cell collection syntax productions when parsing rules because of OOMs in the compiler. We haven't needed to use this syntax since then, but @PetarMax recently identified a lemma that required being able to do so.

Baltoli commented 3 months ago

I verified that KEVM builds successfully with this version of K, and @PetarMax confirmed that it fixes his issue.