Satisfiability solver for constrained Horn clauses (CHC) based on Z3 SMT solver. It combines syntax-guided methods to inductive invariant synthesis with data learning and quantified reasoning over arrays. Find more details at CAV'19 and FMCAD'18 papers.

Compiles with gcc-7 (on Linux) and clang-1001 (on Mac). Assumes preinstalled GMP, and Boost (libboost-system1.74-dev) packages. Additionally, armadillo package to get candidates from behaviors.

• cd aeval ; mkdir build ; cd build
• cmake ../
• make to build dependencies (Z3)
• make (again) to build FreqHorn

The binary of FreqHorn can be found at build/tools/deep/. Run freqhorn --help for the usage info.

FreqHorn does not automatically find counterexamples (unless the CHC system can be trivially simplified), but its supplementary tool expl tool does. We recommend running freqhorn and expl concurrently.

The tools print Success ... if the system is satisfiable.

Collection of the SMT-LIB2 translations of the satisfiable CHC system can be found at bench_horn and bench_horn_multiple. FreqHorn is expected to eventually discover solutions for the systems. On the other hand, there are several unsatisfiable CHC systems at bench_horn_cex, for which freqhorn is expected to diverge (but expl should find counterexamples).