Hi, On my 32-bit machine MRMC gives incorrect timings. This is due to the fact that the clock type is converted to an unsigned long, which is 32-bit on 32-bit systems. A patch follows, which also fixes a typo. By the way, the /new ticket/ link at mrmc-tool.org/trac/wiki/Contact <http://www.mrmc-tool.org/trac/wiki/Contact> doesn't work, because it wants me to log in and I can't seem to make an account. Cheers, Bram Geron CS student at Eindhoven University of Technology --- a/src/io/parser/parser_to_core.c Mon Dec 19 17:13:47 2011 +0100 +++ b/src/io/parser/parser_to_core.c Mon Dec 19 17:28:30 2011 +0100 @@ -103,7 +103,7 @@ } timer_started = FALSE; - return ((unsigned long) (stop_time - start_time) * 1000 + return ((clock_t) (stop_time - start_time) * 1000 + CLOCKS_PER_SEC / 2) / CLOCKS_PER_SEC; } @@ -567,7 +567,7 @@ /* Clean the old results */ clearOldModelCheckingResults(); - /* Star the timer */ + /* Start the timer */ startTimer(); /* In case of simulation engine on we have to traverse the tree */