The current version of the benchmarks:
The benchmarks in TIP format. This is an extension of SMT-LIB with case statements and higher order functions.
In addition, it uses datatypes (which are unofficially standardised),
recursive function definitions from the SMT-LIB v2.5 draft,
and polymorphic definitions as suggested for inclusion to CVC4.
The problems converted to a simpler version of SMT-LIB.
In this version, case statements are turned into if, and higher-order functions
are eliminated using defunctionalisation. Polymorphism is removed by monomorphisation where possible.
Tools for translating from TIP itself or Haskell into other formats like WhyML.