Support multiple solvers for double-checking

[atomb]

This is a bifurcation of #7, since it covered multiple tasks. It would be nice to run all supported solvers to attempt to prove a property, and then check their results against one another for compatibility. Results of "unknown" or "error" would be compatible with any other result, but "sat" and "unsat" would be incompatible. Multiple "unsat" results would be compatible. Multiple "sat" results could use the approach proposed for allsat, returning a list of satisfying assignments.

[dylanmc]

:set prover=any comes close to this, but doesn't do the cross-checking.