Existential quantifiers within Asserts

Mar 29, 2014 at 5:42 AM
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?