The issue comes from reads a[..]. This indicates that any reference could be read, including c1.

Making Dafny know that c1 cannot be accessed solves this issue:

method rowmul(a:array<array<int>>, b:array<array<int>>, c1:array<int>, index:int, indexc: int)
requires abvalid(a, b)
requires 0 <= index < a.Length
requires c1.Length == b[0].Length
requires 0 <= indexc < c1.Length
modifies c1
ensures forall i :: 0 <= i < c1.Length && i != indexc ==> c1[i] == old(c1[i])
ensures c1[indexc] == rowcolmulAux(a, b, index, indexc, 0)
requires forall i :: 0 <= i < a.Length ==> c1 != a[i]
requires forall i :: 0 <= i < b.Length ==> c1 != b[i]
{
    c1[indexc] := rowcolmul(a, b, index, indexc);
}
``