Before the main sort inference, we do a first traversal checking all implicitly scoped parameters
declared with @ or # and infer their sort based on the type they are indexing, e.g., if n was
declared as i32[@n], we infer int for n.
The sort of an application[op](e1, e2) of a primop, which besides the bitwise operations
of prim_op_sort can also be an arithmetic operation on int, i.e., any of the operators
that can be made uninterpreted with uif_ops.