Is this still useful for managed languages? What is a practical use case for this for a Java/python web app?
You can use it to answer questions like "I want to reach this statement in this C# method, what values this method's inputs have to have for the execution to pass all the if checks and so on to reach this statement?".
More broadly speaking, you can use Z3 as a solver for Dynamic Symbolic Execution engine, where DSE is described in:
https://www.microsoft.com/en-us/research/publication/deconst...
Source: I am the first author of "Generating Test Suites with Augmented Dynamic Symbolic Execution" leveraging Z3: https://www.microsoft.com/en-us/research/wp-content/uploads/...
Unless you're implementing solvers or caught up on the particulars of a solver's implementation, the best way to gauge this is to try it.