main/model: move full user-program execution to ModelChecker::run