Index: src/benchmark/bench.h
===================================================================
--- src/benchmark/bench.h	(revision 68e9ace1ce267a16e6490d178a053859919e1241)
+++ src/benchmark/bench.h	(revision 9d32bc86c89192f045f63ab03470624c0d60be7f)
@@ -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