Почему Dafny трудно доказывать свойства с кванторами существования

Попросим доказать очевидное:

method m1()
{
    assert exists y :: 0 <= y <= 100;
}

и получим: assertion violation ! Но почему ? Dafny строит отрицание формулы и пытается опровергнуть полученное отрицание (вспомните курс мат.логики - там делалось то же самое в методе резолюций). В данном случае отрицанием будем формула с квантором всеобщности forall y :: !(0 <= y <= 100). Чтобы ее опровергнуть, надо подобрать такой y, при котором будет нарушено условие !(0 <= y <= 100). Dafny/Z3 воспринимает эту формулу точно так же, как формулу forall y :: P(y), где предикат P можно вычислить, зная значение y, но очень тяжело решить уравнение P(y*) = false относительно y*. Собственно, Dafny и не пытается решать это уравнение. Но тем не менее, в ряде случаев она может сказать, есть ли такой y, что P(y) ложно. Для этого Dafny/Z3 использует так называемую технику matching triggers. А именно, из "контекста" формулы forall y :: P(y) извлекаются все замкнутые термы, которые можно было бы унифицировать с какими-либо подформулами в P (контекст - это по сути состояние прувера - множество всех до этого доказанных формул (их прувер держит "в голове", на всякий случай что они пригодятся в дальнейшем)). Наша формула P не содержит нужных подформул, а вот формула 0 <= f(y) <= 100 такой содержит f(y) и если в контексте будет замкнутый терм f(C), где на месте С будет какое-нибудь число, то Dafny попробует вычислить P при таком y, что f(y) унифицируется с f(C), т.е. при y равном С. Смотрите, как это можно использовать, чтобы подсказать Dafny cправедливость исходной формулы - попробуйте дать ей следующее:

function f(x : int) : int { x }
method m2()
{
   ghost var x := f(17);
   assert exists y :: 0 <= f(y) <= 100;
}

Как будто бы ничего не изменилось по сравнению с методом m1, однако теперь Dafny говорит заветное
"Dafny program verifier finished with 3 verified, 0 errors"