[move-prover] Unpredictable behavior with different vector lengths

[jyao15]

The verify_sort.move test program implements a vector sorting algorithm. Currently the vector length is set to 45 and the program is successfully verified by Move. When we change the length to some larger numbers (e.g., 100), the prover will time out. This may be a Z3 issue unrelated to the Move prover. However, if we change the length to certain numbers (e.g., 148 or 1000), the Move prover will throw error: induction case of the loop invariant does not hold on invariant forall k in i+1..j: v[i] <= v[k]. The error appears to be fake. I translated the same program and loop invariant to Dafny (see array_sorting.dfy.txt). Dafny verified the program without error in two seconds.