Verification condition in case of array theory
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.