Empty type initialization leads to proving false

[MikaelMayer]

trafficstars

Dafny version

4.4 nightly

Code to produce this issue

type Empty = x: int | false witness *

class TestEmpty {
  const x: Empty
  constructor() ensures false {
    x := 2;
    new;
  }
}

Command to run and resulting output

Paste in VSCode

What happened?

It verifies. It should not. See https://github.com/dafny-lang/dafny/issues/2727#issuecomment-1972056465 for why it can verify.

What type of operating system are you experiencing the problem on?

Windows

[MikaelMayer]

It also works if I replace "const" by "var"

[RustanLeino]

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

[RustanLeino]

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()), 

This where clause should not be there! Instead, this condition in this where clause should be placed in an assume statement together with

assume !$Unbox(read($Heap, this, alloc)): bool;

which is part of the translation of new;.

[RustanLeino]

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 the postcondition.

The where clause in Call$$_module.TestEmpty.__ctor, however, should remain.