+int main_argc;
+char **main_argv;
+
+/** The real_main function contains the main model checking loop. */
+static void real_main() {
+ thrd_t user_thread;
+ struct model_params params;
+
+ param_defaults(¶ms);
+
+ parse_options(¶ms, &main_argc, &main_argv);
+
+ //Initialize race detector
+ initRaceDetector();
+
+ //Create the singleton SnapshotStack object
+ snapshotObject = new SnapshotStack();
+
+ model = new ModelChecker(params);
+
+ snapshotObject->snapshotStep(0);
+ do {
+ /* Start user program */
+ model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
+
+ /* Wait for all threads to complete */
+ model->finish_execution();
+ } while (model->next_execution());
+
+ delete model;
+
+ DEBUG("Exiting\n");
+}