Dwight, we cannot simply mimic smtlib, because smtlib does not differentiate between singed and unsigned value.