Integration with other SMT solvers

[LeventErkok]

Consider integrating with

• CVC3 (http://cs.nyu.edu/acsys/cvc3/)
• Boolector (http://fmv.jku.at/boolector/)
• STP (http://sites.google.com/site/stpfastprover/)
• MathSat (http://mathsat4.disi.unitn.it/)
• Z3 (http://research.microsoft.com/en-us/um/redmond/projects/z3/)

• OpenSMT (http://verify.inf.unisi.ch/opensmt)

  Potential issues:

• MathSat is not open-source
• Z3 is Windows only
• OpenSMT has QF_BV support but not QF_AUFBV

[LeventErkok]

looks like we're committing to Yices and Z3; but with the SMTLib2 backend others can be added with relative ease; if someone really needs it.