HiFrog is a bounded Model Checker for C programming language which is based on  SMT solver OpenSMT2.  

HiFrog is a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language for verifying a set of user-defined assertions in a single program. 

The tool supports quantier-free theories of  three encoding precisions through SMT:

• Equality with Uninterpreted Functions (EUF), 
• Linear Real Arithmetic (LRA),
• Linear Real Arithmetic (LIA),
• Propositional Logic(PROP).

HiFrog exploits the CProver framework and inherits some of its options.