Multiple fixes to the type inference
 - enforce certain types for icmp and select
 - Minimize type models to avoid infinite loops when Z3 does not deliver minimal models