The values of ownership variables inferred by Z3 are then substituted into the
constrained Horn clauses, and the resulting system is checked
for satisfiability with an off-the-shelf CHC solver.
Our implementation generates constraints in the industry standard
SMT-Lib2 format [1]}; any solver that accepts
this format can be used as a backend for ConSORT. Our implementation
currently supports Spacer [2]} (part of the Z3 solver [3]}),
HoICE [4]}, and Eldarica [5]}
(adding a new backend requires only a handful of lines of glue code).
We found that different solvers are better tuned to different problems;
we also implemented parallel mode which runs all supported solvers
in parallel, using the first available result.
