function lemma in "ensures" doesn't work in 1.9.8 (worked in 1.9.7)

[xinhaoyuan]

The third lemma doesn't verify:

lemma lemma_Subset_Cardinalities<I>(a : set<I>, b : set<I>)
    ensures a <= b ==> |a| <= |b| && |b - a| == |b| - |a|
{
    if (a <= b) {
        if x :| x in a {
            assert x in b;
            lemma_Subset_Cardinalities(a - {x}, b - {x});
        }
        else {
            assert a == {};
            assert |b - a| == |b| == |b| - |a|;
        }
    }
}

predicate pred_lemma_Subset_Cardinalities<I>(a : set<I>, b : set<I>) 
    ensures a <= b ==> |a| <= |b| && |b - a| == |b| - |a|
    ensures pred_lemma_Subset_Cardinalities(a, b) 
{
    lemma_Subset_Cardinalities(a, b);
    true
}

lemma lemma_Subset_Cardinalities_Universal<I>()
    ensures forall a : set<I>, b : set<I> :: a <= b ==> pred_lemma_Subset_Cardinalities(a, b) && |a| <= |b| && |b - a| == |b| - |a|
{
}

while function lemma in body is still working in 1.9.8:

lemma lemma_Subset_Cardinalities_Universal<I>()
    ensures forall a : set<I>, b : set<I> :: a <= b ==> |a| <= |b| && |b - a| == |b| - |a|
{
    if a : set<I>, b : set<I> :| a <= b && !(|a| <= |b| && |b - a| == |b| - |a|) {
        assert pred_lemma_Subset_Cardinalities(a, b);
    }
}

[seanmcl]

Still a problem at master.

[acioc]

Investigating this issue will be done for Dafny 3.0

[cpitclaudel]

This bug was fixed in Dafny 3.1, and remains fixed in 3.6 🎉
I will add it to the test suite to make sure that it remains so.