Daejun Park

I admit that the translation is not correct. I realized the problem soon after I encoded it in that way, but I postponed fixing it since I wanted to think/discuss...

@grosu Your encoding seems to work, although I haven't thought about it that much. But, my original question is how to incorporate the `requires` and `ensures` that are not local....

Probably, no. From what I remember, `getKLabel` doesn't work.

Sorry for the delay in replying. You can declare a list whose elements are separated by white spaces, as follows: ``` syntax YouList ::= List{YourElem, ""} ``` Note that K...

You can increase the JVM memory size by providing, for example, ``` K_OPTS=-Xmx4g ```

@mragankyadav Unfortunately, it is not available yet. Sorry for your inconvenience.

@radumereuta any idea?

This problem frustrates me in porting JavaScript semantics into K4.0, especially because I cannot initialize the configuration with a large number of built-in JavaScript objects.

@dwightguth yes, it still happens in rv-k: ``` $ kompile --version K framework version 1.0-SNAPSHOT Git revision: 9f04b6c Git branch: master Build date: Thu Jun 09 16:39:42 CDT 2016 ```

A possible workaround is to use explicit klabel, i.e., `#cells` for Bag, `_Map_` and `_Set_` for Map and Set, like: ``` rule @InitConfig => . ... (.Bag => #cells( 1...