Rustan Leino

The `where` clause of parameter `this` in the `CheckWellFormed$$` procedure for Dafny constructors should _not_ include `$IsAlloc(this, Tclass._module.Test(), $Heap)`. In fact, we should make `this` be an out-parameter of such...

By "works", do you mean that using "var" also shows the unsoundness or that there is no soundness issue when you use "var"?

I think the problem is that the constructor is translated into Boogie as: ``` procedure {:verboseName "TestEmpty._ctor (correctness)"} Impl$$_module.TestEmpty.__ctor(m#0: int) returns (this: ref where this != null && $Is(this, Tclass._module.TestEmpty()),...

The `where` clause should also be removed from the `CheckWellFormed$$_module.TestEmpty.__ctor` procedure. Instead, the body of that procedure should assume the condition at the break between checking the precondition and checking...

Thanks you for the many useful test cases! (Note from @keyboardDrummer: this is indeed a bug) ## Workaround As a workaround, adding any one of these three statements in the...

## Summary General functions (that is, `~>` arrow types) are difficult to work with. I don't know of a good way to legally write the body of `closed()` as intended....

@cpitclaudel Sorry, I must have lost the rest of the example. But your example is good, and also I reconstructed a repro for when the function result is named. It...

Nice sleuthing! The crash you're seeing is a bug in Boogie. Here is a smaller repro: ``` boogie function {:never_pattern true} P(x: int): bool; procedure Test() { assert (forall xyz:...

Hi @fabianhauser @kailingP . Sorry, I got here a bit late. From what I'm hearing, the problem with #66 was that the .zip files can't be properly unzipped. Do we...