Binding guard assumes type condition too early

[RustanLeino]

Dafny version

4.10

Code to produce this issue

type MayBeEmpty

lemma Test() {
  if e: MayBeEmpty {:trigger} :| true {
  } else {
    // BUG: Evidently, false is provable here, but it shouldn't be
    assert false;
  }
}

Command to run and resulting output

// Here's a longer example that shows the verified program crashes at run time.
//
// > dafny run test.dfy

module M {
  export
    provides Empty, False
  
  type Empty = x: int | false witness *

  lemma False(e: Empty)
    ensures false
  {
  }
}

lemma GiveMeEmpty() returns (ee: M.Empty)
{
  if e: M.Empty {:trigger} :| true {
    ee := e;
  } else {
    // BUG: Evidently, false is provable here, but it shouldn't be
    assert false;
  }
}

method Main() {
  var e := GiveMeEmpty();
  M.False(e);
  print 10 / 0; // crashes at run time
}

What happened?

The Boogie generated for the if e: T | P(e) ... has the following form:

  var e#0_0: Box
    where $IsBox(e#0_0, Tclass.M.Empty()) && $IsAllocBox(e#0_0, Tclass.M.Empty(), $Heap);
  ...
  havoc e#0_0;
  if (*) {
    assume P(e#0_0);
    ...
  } else {
    assume !(exists e :: $IsBox(e, Empty) && P(e));
    ...
  }

The variable e#0_0 should not have a where clause. Instead, that condition should be moved to be an assumption just inside the then branch of the if.

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

Mac