mu-mmint: Add checks before running the smtlib encoder

 * Add formula ids if needed and overwrite model
 * Detect if model is may only
 * Change suffix of concretization to _example