Add static (i.e. compile-time) type reflection

This patch uses SMT-Kit's internal reflection features to
deduce type information about internal and external variables.
Illustrate rudimentary loop unwinding