The input programs are C programs operating on ints. They are translated to the integer programs described in the paper using the tool llvm2kittel. Note that in the green header, our web interface only outputs bounds in the TermComp format (i.e., here it cannot display polynomial-logarithmic bounds).
For more precise bounds, please refer to the "All Bounds" section at the end of the generated proof.