Cosmin Radoi

When the rewrites are local, I think the correct translation is to simply leave them there. Unless I'm missing some subtlety, `body AND (requires => ensures)` should work in all...

it looks like non-determinism. Could you --search to figure out what's going on?

@bmmoore, assigned you so we have someone tracking this issue.

@bmmoore implemented most of this so he understands the various data structures much better. I'll forward a link to this issue to his email.

@dwightguth, this seems related to the binary serialization change

@imran-iitp, the --pdf option is not available in K 4.0 yet. We are working on it and it should be there in a few weeks.

@omarz1, it would be great if you could pick this up. We are working on a new API for K and this would be a good opportunity to exercise the...

@jsinglet, it's been on our todo list for a while but we didn't get to it. In some cases it's possible to compile the same program with K 3.6, and...

@daejunpark, as far as I remember, we made `List{...}` assoc at some point. So the original version should have worked.

this looks like an issue with concretization, not assoc. ``` rule (H:HeaderTypeDeclaration => .) ... ``` ``` rule (H:HeaderTypeDeclaration => .) _ ``` should be identical after compilation. @kheradmand, does...