SMT + Types

[renau]

-Bitwidth inference using SMT (min/max bits)

-Assertions "I"/"N", are placed to help constraints

-Provide a failing example

-Maybe a MAXSAT example? to report an error. For error reporting, the inputs/outputs per module and the LoC
that violates the constraint may be an better way to debug.