Add support for constant expressions as operands
This commit also shuffles some code around, but without any other functionality change
specialize icmp comparison per %reg
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
switch to Z3 SimpleSolver for solving type constraints