*Complexity Integer Term Rewrite Systems* are a special form of integer term rewrite systems that is used for complexity analysis. For further details, we refer to our paper at TACAS 2014. Each `cint` file consists of four parts:

- The declaration
`(GOAL COMPLEXITY)`

, specifying that the goal of this file is complexity analysis. - The list of start states
`(STARTTERM (FUNCTIONSYMBOLS`

. Currently, only one state (e.g.,*start*))*start*) may be specified as a start state. - The declaration of all variables that are used in the remaining program.
This includes not only the variables representing the state of the program,
but also all variables that are only used to define constraints. The list of
variables is space-separated. Hence, the line
`(VAR A B C D)`

declares the variables`A`

,`B`

,`C`

, and`D`

. - Finally, the list of transitions, given in the statement
`(RULES ...)`

. Each transition consists of a start state, an arrow (`->`

), a list of end states (wrapped in`Com_`

, where*k*(...)*k*is the number of end states), and an optional constraint separated by`:|:`

from the rest of the state. The start state is given in the form`f(X`

where_{1},...,X_{n})`X`

is the_{i}`i`

th variable of the program (for`1 <= i <= n`

). Each of the end states is given as`f(t`

where_{1},...,t_{n})`t`

is the value of the_{i}`i`

th variable after evaluating the transition (for`1 <= i <= n`

). All values and constraints have to be given as polynomials over the variables in the`(VAR ...)`

section. Variables occurring in an end state, but not in the start state are interpreted as an arbitrary integer.