These days, in automated program verifications, it is fashionable to pose problems as the solution to a system of Horn clauses, where most Horn clauses define the inductiveness conditions for an invariant, and then some constraint define the safety conditions to match.
One file format for this is SMT-LIB: the clauses are just assert statements over predicates, considered as functions mapping to Booleans.
Solvers implementing this include vanilla Z3 and Spacer.
What are the other reasonably mature, documented and downloadable solvers capable of solvings such problems?
Even Z3 has multiple solvers, e.g., BMC, PDR (the default?), CLP (prolog-style reasoning), Datalog, and Duality. Choose with fixedpoint.engine=xx. There's also another engine coming soonish which is a port of HSF to Z3. (the original HSF is also available and is very reliable)
There are other solvers out there, but I don't have much experience with them. E.g., Eldarica, VeriMAP, etc.