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?
