The solvers were run on the StarExec platform [1]} with a dedicated cluster of 12 nodes,
where each node consisted of two 4-core 2.4 GHz Intel processors with 256 GB RAM and 1 TB hard-disk space.
The memory usage limit for each solver run was set to 128 GB, and the wall-clock time limit is set to 3600 seconds
(thus, a solver that used all 4 cores could consume at most 14400 seconds of CPU time).
The solutions that the solvers produced were checked for both syntactic and semantic correctness.
That is, a first postprocessor checked that the produced expression adhered to the grammar specified in the given benchmark,
and if this check passes, a second postprocessor checked that the solution adhered to semantic constraints
given in the benchmark (by invoking an SMT solver).
