Andrei Stefanescu

Can you try this path `/Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5` (without `int-kompiled`)?

It's the same bug as @ehildenb reported. I should fix it :-)

@traiansf yes, this is a limitation of the prover. A better way of phrasing it is that the prover assumes that the semantics is "complete". In theory, the condition can...

I am looking into it. The issue is not one of non-determinism, because `stmt` should be cooled.

This is a limitation of current implementation: associative and commutative matching is compiled to associative only matching, and having a side condition on `A` is not supported. For now, maybe...

Ok, I will take a look over the weekend and get back to you.

The exception is generated by applying this rule ``` rule lvalue Id => ref(!L) ... Loc:Map (.Map => Id |-> Loc[!L]) requires (notBool(Id in keys(Loc))) ``` on the term ```...

@grosu I created this issues based on my recollection of what we discussed. @radumereuta maybe you guys can talk and figure out what the problem is.

This does not block the release of the tutorial.