Atc-boolean-from-integer-return-rules
Rules about the return types of boolean-from-<type>.
We also include the type prescription rules for these functions.
The reason is that we have observed that,
in the presence of the non-strict operators && and ||,
the symbolic execution may produce
equalities between t and calls of these functions,
under a hypothesis that the call holds (i.e. is not nil).
This situation arises because of the case splits engendered by
the rules for exec-expr-pure on && and ||
and the rules for test-value.