[CHY872]

Coq already could, if they wanted to. Z3 supports the SMT-Lib format, which means that any theorem prover that can both output that and execute a shell command can invoke Z3. This has no bearing on Z3's specific license, unless you want to use that tool for commercial purposes. For an example of this being used in a similar tool to Coq, Isabelle/HOL's 'Sledgehammer' tactic will attempt to use Z3 (and then reconstruct a proof) where its own solvers fail.

It's all pretty nifty!

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.306...

HOL4 also has Z3 (and Yices) support, but I think the Z3 support is a little out of date (in particular, it errors immediately on start).