Believe it or not, a very good example of such a language which you might be familiar with is SQL.
SQL is declarative only when you don't care about data integrity and performance.
Maybe a bit better example for this kind of behavior are compilers. They're pretty "declarative" these days. You write what code you want to compile, and the compiler will pass it through a thousand transformation stages, deciding which trick to apply at every instruction, which code isn't really needed and so on.
Of course, then you also need to deal with compilers getting it wrong too, so you start tweaking your code with special words like "volatile" and "restricted", mess with compiler options, and sometimes even disassemble code to see why turning the "fast" options makes your code slow. But in general, high quality compilers do this dance way better than SQL.
So what's the moral here? Two things.
First, calling something "declarative" doesn't really mean anything. It means the language is built on a very thick abstraction that lets the computer do more work than usual, so you can do less work.
Second, thick abstractions are leaky. Works for basic cases, past that you'll still end up doing a lot of work, but now you have to fight your computer while doing it, as well.
The Z3 Theorem Prover is an interesting toy, but I wouldn't trust it to do anything right in the real world. Much like most Microsoft Research projects, unfortunately.
If you have never tried it out you should, maybe you will like declarative languages a little bit more afterwards.
Also I wasn't suggesting that declarative languages are broadly useful (in fact I'd suggest quite the opposite), just that they are very interesting.
Granted I've only used it in one university course (and only half of that course).