#1216 CIF to BDD: support binary '*' / 'sign' on a real-typed value is not supported.

• Best to review per commit.
• End-user visible changes:
  • The CIF data-based synthesis tool and the CIF controller properties checker (for BDD-based checks) now support multiplication (binary * operator).
  • The CIF data-based synthesis tool and the CIF controller properties checker (for BDD-based checks) no longer crash on using the sign function on a real-typed value. It is still unsupported (except if it can be statically evaluated), but it now properly reports the problem rather than crashing.

Addresses #1216 (closed)