haRVey is a SMT (Satisfiability Modulo Theories) prover. There are presently two branches of haRVey: haRVey-SAT and haRVey-FOL.

• haRVey-FOL integrates a First-Order Logic theorem prover (hence its name), i.e. the E-prover. It uses the superposition calculus as implemented by the E-prover, to determine the satisfiability of Boolean combinations of atoms with functions interpreted in a first-order theory with equality.
  

• haRVey-SAT is based on congruence closure, the Nelson-Oppen framework, and rudimentary instantiation techniques to decide the satisfiability of a set of atoms written with uninterpreted symbols, linear arithmetics, some lambda-expressions, and some quantifiers. The Boolean engine is a SAT solver (zChaff or MiniSAT), hence its name.
  

• License:
  
  • haRVey-FOL: GNU LGPL 2.1
    
    • haRVey-FOL relies on E-prover (http://eprover.org/): GNU GPL
      
  • haRVey-SAT: BSD like
    
    • haRVey-SAT relies on MiniSat(http://minisat.se/): BSD like
      
• Web site: http://harvey.loria.fr/haRVey.php