Regression in set reasoning

[jaylorch]

The following code verifies with Dafny 3.0.0. But it doesn't verify with Dafny 3.1.0 or with the latest commit.

module M {

  datatype D = D(v: int)

  function Identity(x: int) : int
  {
    x
  }

  function SeqToSet(ds:seq<D>) : set<int>
  {
    set d | d in ds :: Identity(d.v)
  }

  lemma Lemma_SeqToSetEmpty(ds:seq<D>)
    requires (set d | d in ds :: d.v) == {}
    ensures  |SeqToSet(ds)| == 0
  {
    var s := SeqToSet(ds);
    if (|s| > 0)
    {
      var d' :| d' in ds;
      assert d'.v in (set d | d in ds :: d.v);
      assert d'.v !in {};
      assert (set d | d in ds :: d.v) != {};
      assert false;
    }
  }

}

[RustanLeino]

Thanks for the bug report. Until this gets fixed, here's a workaround:

lemma Lemma_SeqToSetEmpty(ds:seq<D>)
  requires (set d | d in ds :: d.v) == {}
  ensures  |SeqToSet(ds)| == 0
{
  var s := SeqToSet(ds);
  if (|s| > 0)
  {
    var D := set d | d in ds :: d.v;
    var d' :| d' in ds;
    assert d'.v in D;
    assert false;
  }
}