Gather additional solvers and configurations for experiments

[delcypher]

We should compare against as many available solvers that support floating-point/bitvectors as possible.

Floating point

COLIBRI

Winner of SMT-COMP 2017 QF_FP division

https://www.starexec.org/starexec/secure/details/solver.jsp?id=12031

I should check the license on this and whether this is the right version.

TODO: Read this paper!

http://smt-workshop.cs.uiowa.edu/2017/papers/SMT2017_paper_21.pdf

http://soprano-project.fr/download_colibri.html

GoSat

https://github.com/abenkhadra/gosat

Similar to XSat, but open source, uses LLVM to JIT code and uses different optimization libraries.

MathSat5

Need to ask Alberto Griggio or Mikhail Ramalho for optimal configuration for floating-point constraints.

XSat

Paper: http://zhoulaifu.com/wp-content/papercite-data/pdf/xsat.pdf

SMT-COMP submission:
http://smtcomp.sourceforge.net/2017/systemDescriptions/XSat.pdf
https://www.starexec.org/starexec/secure/details/solver.jsp?id=11647

Z3

We already support this. We'll just use Z3's default behaviour.

BitVectors

Given JFS's weakness here I'm not sure if it's worth comparing to that many solvers.