Termite is a tool to check termination of programs in the LLVM IR. It uses pagai as invariant generator and Z3 as SMT-solver.
Using opam, you can install (most of) the dependencies easily. See the install instructions here.
External dependencies:
- Z3
- Pagai
Ocaml dependencies: