Base type throws off witness checking

[RustanLeino]

Dafny version

4.6.0

Code to produce this issue

type Empty = x: int | false witness *

method OperateOnEmpty(x: Empty)
  ensures false
{
}

type PurportsToBeNonempty = x: Empty | true
  witness 506 // BOGUS: this is not a witness, and yet no error is reported

method Main() {
  var x: PurportsToBeNonempty := *;
  OperateOnEmpty(x);
  print 10 / 0; // boom!
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 3 verified, 0 errors
Unhandled exception. System.DivideByZeroException: Attempted to divide by zero.
   at System.Numerics.BigInteger.op_Division(BigInteger dividend, BigInteger divisor)
   at System.Numerics.BigInteger.Divide(BigInteger dividend, BigInteger divisor)
   at Dafny.Helpers.EuclideanDivision(BigInteger a, BigInteger b)
   at _module.__default._Main(ISequence`1 __noArgsParameter)
   at __CallToMain.<>c__DisplayClass0_0.<Main>b__0()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)

What happened?

The verifier sets up the witness check for PurportsToBeNonempty incorrectly. In particular, it performs the check under the assumption that there is an x: Empty, whereas it should be checking that such an x exists. In more detail, the bug stems from the Boogie where clause given to x. The fix is to remove the where clause and to instead assume x: Empty not for the witness check, but only for the well-formedness check of the constraint.

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

Mac