Building SMT-based Software Model Checkers: an Experience Report