Empty type of let variable assumed before binding

[RustanLeino]

The following program verifies, but should not:

type R = r: BaseType | r.i() witness *

function F(v: nat): R {
  var o: R := Ctor(v);
  o
}

The following similar code, but without the let expression, does produce an error (which is good):

function G(v: nat): R {
  Ctor(v) // error: This does not produce an R
}

A quick look at the generated Boogie shows that var o: R ... generates an assumption about o's type before the RHS has been evaluated and checked. That assumption should not be there (at least for a possibly empty type).

[cpitclaudel]

@RustanLeino it looks like your OP is missing some context. Do you still have the full example?

In the meantime, here's one possible completion:

type BaseType {
  predicate i()
}

function Ctor(x: nat) : R
  requires exists b: BaseType :: b.i()
{ var b : BaseType :| b.i(); b }

type R = r: BaseType | r.i() witness *

function F(v: nat): R {
  var o: R := Ctor(v);
  o
}