Z3 (and other constraint solvers) are very impressive. The most interesting application I've seen is in binary exploitation and reverse-engineering through symbolic execution.

Angr is a very popular framework which allows for symbolic execution of binaries using Z3 as a backend. It's made a whole class of common CTF challenges almost trivial:

https://docs.angr.io/docs/examples.html

Absolutely!

Not to mention the often impressive performance of "general" MIP solvers. It is only a shame that the best ones there are commercial (Gurobi followed by Cplex). That said, Cbc is lovely in a wide range of cases, and is open-source.

I always thought "NP-complete/NP-hard" metaphor only meaningful in theoretical work. In practice, it does not make much sense in guiding what/how the real world problem is to be solved.

I don't know. I find it useful in practice. Apart from anything else it means there's (probably) no point looking for an exact polynomial-time algorithm, which can save a lot of wasted effort. But it also gives useful clues about what sort of algorithmic approaches might be useful, and allows you to relate your problem to a huge amount of existing research.

It's really basic taxonomy: what sort of problem are we dealing with? If you don't know that, how could you even begin to design a reasonable algorithm for it?

Maybe you are heavily on huge algorithmic work. In practice, most algorithms are polynomial-time, and we are looking for under-polynomial-time alternative - log(n). For exponential-time, we are just looking for an approximate alternative.