Forest

Forest implements symbolic execution of LLVM intermediate language and is able to detect errors in programs developed in C. Forest transforms a program into a set of SMT formulas describing each feasible path and decides these formulas with a SMT solver. This enables to prove the satisfiability of reachability conditions such as the ones presented in svcomp. Forest implements different encodings of SMT formulas, according to different theories: linear arithmetic, polynomials and generic bit-accurate and not bit-accurate translations.