Дафни, вызов может нарушать условие изменения контекста

В моей программе (полная версия на rise4fun) я хочу разделить массив, отсортировать каждый фрагмент и затем объедините их вместе.

Я решил использовать последовательности, потому что это упрощает нарезку и слияние. Затем, чтобы повторно использовать некоторый существующий код, я преобразовываю каждый фрагмент в массив и вызываю свою реализацию сортировки вставками. Но вызов сообщает об ошибке call may violate context's modifies clause. Почему это?

Вот основная часть моего кода.

method MySort(input:array?<int>)
modifies input;
requires input != null;
requires input.Length > 0;
requires input.Length%2==0;
{
if(input.Length%2!=0){return;}
 var mid:int := input.Length/2; 
 var subOne := input[0..mid];
 var subTwo := input[mid..input.Length];
 var arrSubOne := toArrayConvert(subOne);
 var arrSubTwo := toArrayConvert(subTwo);
 insertionSort(arrSubOne); //call may violate context's modifies clause
 insertionSort(arrSubTwo); //call may violate context's modifies clause
} 

method toArrayConvert(s:seq<int>) returns(a:array<int>)
requires |s|>0;
ensures |s| == a.Length;
ensures multiset(s[..]) == multiset(old(s[..]))
ensures forall i::0<=i<a.Length ==> s[i] == a[i];
{ /* ... */ }

method insertionSort(input:array?<int>)
modifies input
requires input != null
requires input.Length > 0
ensures perm(input,old(input))
ensures sortedBetween(input, 0, input.Length) // 0 to input.Length = whole input
{ /* ... */ }