[quesomaster9000]

Z3 is entirely different IMHO, once you get into solvers the question becomes not just 'is this satisfied' but 'what is the minimum sequence of steps necessary to arrive at the result'.

I have relied heavily on both Z3 and Alloy for ad-hoc jobs, and Prolog doesn't even come close to the inference power, and that's along-side Macsyma and Sage.

[rscho]

The big advantage of prolog vs solvers is the logic programming aspect. If you can express parts of your program in a logically pure way, Prolog code will be much more concise than the Z3 equivalent, although probably slower. Another advantage is that Prolog outputs and reads Prolog terms, which makes it very good for metaprogramming. It's like lisp: incredible if you're solo prototyping, not so much if you're part of a team of corporate cogs.

[Karrot_Kream]

What problem domain are you working in? I find usage of solvers and Prolog to be very domain specific.

[quesomaster9000]

At the moment I'm verifying a Rust floating point implementation, which has lead to many small snippets for not just generating test & edge cases (e.g. find inputs which falls outside of these conditions), but trying to prove completeness on all valid inputs.

[gatlin]

Have you tried sCASP?

[rurban]

Most better prologs now include solvers already.