Verification condition in case of array theory As far as i can understand the problem of checking safety property, can be reduce to solving for inductive invariants in VC's and there is following parts to it:


Generate VC's from the program.
Solve it: If user provide inductive invariants just check the Validity of the whole VC formula. 
Inferring problem : simultaneously solve the VC's taking these predicates as uninterpreted function that make all the VC's valid.


How hard the problem of checking 2. (User provide the inductive invariant) in the case of array theory? For example: Array sorting.
Sure, if the user provides inductive invariants, you can try to check the validity of the verification conditions.  However, this remains undecidable, as it requires checking the validity of a formula in first-order logic (with quantifiers and array expressions), and that's undecidable.

It might be feasible often enough in practice to be useful, especially since we might hope that programmers have a reason why their code is correct and won't write code that requires overly complex reasoning to prove correct.  But in general, it is undecidable.