**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.