These benchmarks were generated by r_type and encode correctness of functional programs, most of them higher-order. All problems are encoded in the SMT-LIB 2 Horn logic, and start with a set-info containing the program they come from.
See also the original repository.
Adrien Champion (University of Tokyo)