Questions about SMT logic solvers

[olgerm]

Are smt-solvers (like z3) theoretically able to (always correctly) check consistency of any 1.-order logic formula?
Does it follow from The undecidability of first order logic, that an algorithm, that could check consistency of any 1.-order logic formula, does not exist?
How does the algorithm of work in details? (link to explanation)
Are there any algorithms that could check consistency of any 2.-order logic formula?
Does Gödels 2. incompleteness theorem claim, that such algortihm, that could check consistency of any 2.-order logic formula, does not exist.
Are there any computerprograms that could check consistency of any 2.-order logic formula?

To explain what I mean by 1.-order logic formula I will write here a few examples:

• $\exists_{x_1}(A(x_1))\land \neg \exists_{x_1}(A(x_1))$
• $\exists_{x_1}(\exists_{x_2}(A(x_1,x_2)\land \exists_{x_3}(A(x_2,x_3)\land A(x_2,x_2))))\land \neg \exists_{x_1}(\exists_{x_2}(\exists_{x_3}( A(x_2,x_1)\land A(x_1,x_3)\land A(x_1,x_1))))$
• $\exists_{x_1}(m(x_1) \land \neg\exists_{x_2}(M(x_1, x_2) \land \exists_{x_3}(M(x_1, x_3) \land \neg M(x_2, x_3) \land M(x_3, x_1)) \land \exists_{x_3}(M(x_1, x_3) \land M(x_2, x_3)) \land \neg \exists_{x_3}(M(x_2, x_3) \land M(x_3, x_3))))\land \exists_{x_1}(\exists_{x_2}(m(x_2)\land M(x_2,x_1)\land \exists_{x_3}(M(x_1,x_3)\land M(x_2,x_3))\land \exists_{x_3}(M(x_2,x_3)\land M(x_3,x_2)\land \neg M(x_1,x_3)))\land \neg \exists(M(x_2,x_1)\land M(x_2,x_2)))\lor\exists_{x_1}(M(x_1,x_1)\land \neg \exists_{x_2}(M(x_1,x_2)\land M(x_2,x_2)\land M(x_2,x_1)))$

 

[olgerm]

I have an idea for smt-solver algorithm myself. Some details are still unclear. It is quite long. I can not post it here very well. Were do you think I could find someone who were interested of it? Should I contact makers of z3?

 

[olgerm]

Which mathematical problems z3 can not solve? (I am asking a few examples of simpler mathematical problems/tasks, that z3 can not solve)?