dafny сбой предварительного условия

• Я пытаюсь запустить проверенную версию BFS (от здесь)
• Мой входной график в полном порядке, но по какой-то причине он не проходит предварительную проверку.
• Вот постоянная ссылка
• И для полноты вот определение графика + условия достоверности

class Graph
{
    var adjList : seq<seq<int>>;
    constructor (adjListInput : seq<seq<int>>)
    {
        adjList := adjListInput;
    }
}
function ValidGraph(G : Graph) : bool
    reads G
{
    (forall u :: 0 <= u < |G.adjList| ==> forall v   :: 0 <= v <     |G.adjList[u]| ==> 0 <= G.adjList[u][v] < |G.adjList|) &&
    (forall u :: 0 <= u < |G.adjList| ==> forall v,w :: 0 <= v < w < |G.adjList[u]| ==> G.adjList[u][v] != G.adjList[u][w])
}
method main()
{
    var G : Graph := new Graph([[1,2],[0,2],[0,1]]);
    assert (ValidGraph(G));
}

• Дафни отвечает Error: assertion violation