Index: kernel/generic/src/console/cmd.c
===================================================================
--- kernel/generic/src/console/cmd.c	(revision 34db7fa828e4d10ee2a902fb4143704b3feda184)
+++ kernel/generic/src/console/cmd.c	(revision 4c3b7972679b8fbe6de66a73d7a09c1e266432b6)
@@ -68,8 +68,4 @@
 #ifdef CONFIG_TEST
 #include <test.h>
-#endif
-
-#ifdef CONFIG_BENCH
-#include <arch/cycle.h>
 #endif
 
@@ -866,12 +862,26 @@
 {
 	printf("%s\t\t%s\n", test->name, test->desc);
-#ifdef CONFIG_BENCH
-	uint64_t t0 = get_cycle();
-#endif
+	
+	/* Update and read thread accounting
+	   for benchmarking */
+	ipl_t ipl = interrupts_disable();
+	spinlock_lock(&THREAD->lock);
+	thread_update_accounting();
+	uint64_t t0 = THREAD->cycles;
+	spinlock_unlock(&THREAD->lock);
+	interrupts_restore(ipl);
+	
+	/* Execute the test */
 	char * ret = test->entry();
-#ifdef CONFIG_BENCH
-	uint64_t dt = get_cycle() - t0;
+	
+	/* Update and read thread accounting */
+	ipl = interrupts_disable();
+	spinlock_lock(&THREAD->lock);
+	thread_update_accounting();
+	uint64_t dt = THREAD->cycles - t0;
+	spinlock_unlock(&THREAD->lock);
+	interrupts_restore(ipl);
+	
 	printf("Time: %llu cycles\n", dt);
-#endif
 	
 	if (ret == NULL) {