Dafny gives assertion violation for asserts with predicates having an existential quantifier.
For example consider a simple example below which is true but dafny gives an assertion violation.
static method Main1(a:array<int>)
requires a != null && a.Length > 0;
assert (exists x:int:: 0<= x < 5);
Is it possible to use predicates with existential quantifiers within asserts?