Index: src/benchmark/bench.h
===================================================================
--- src/benchmark/bench.h	(revision 399a908cc97cdaad27d16bbf3d5672d0e4db6110)
+++ src/benchmark/bench.h	(revision d28a03ecbd43a9006978a2f77f2752fc4daadd7d)
@@ -6,5 +6,8 @@
 	#include <stdlib.h>
 	#include <unistd.h>					// sysconf
-#if defined(__cforall)
+#if ! defined(__cforall)
+	#include <time.h>
+	#include <sys/time.h>
+#else
 }
 #include <time>
@@ -39,11 +42,13 @@
 	}						\
 	long long int StartTime, EndTime;	\
-	StartTime = bench_time();			\
+	StartTime = bench_time();		\
 	statement;					\
-	EndTime = bench_time();				\
+	EndTime = bench_time();			\
 	unsigned long long int output = 	\
 	( EndTime - StartTime ) / n;
 
+#if defined(__cforall)
 Duration default_preemption() {
 	return 0;
 }
+#endif