Rules about sint-from-boolean.
We expand sint-from-boolean, because it is really just an abbreviation. In fact, we want to expose its if structure in the symbolic execution.