Simplification of VCs (helping Z3 in a few instances). We emit a
special function instead of the disjunction. In the future this
might be replaced by fp.isFinite anyway.

Change-Id: I7fa66d65431fa8b41ff23c6d46a6586d9e8f8081