diff --git a/hermit/usr/benchmarks/basic.c b/hermit/usr/benchmarks/basic.c
index f0f611031..5794226ad 100644
--- a/hermit/usr/benchmarks/basic.c
+++ b/hermit/usr/benchmarks/basic.c
@@ -62,24 +62,15 @@ void reschedule(void);
 
 static char* buff[M];
 
-#if 0
-inline static unsigned long long rdtsc(void)
-{
-	unsigned long lo, hi;
-	asm volatile ("rdtsc" : "=a"(lo), "=d"(hi) :: "memory");
-	return ((unsigned long long) hi << 32ULL | (unsigned long long) lo);
-}
-#else
 inline static unsigned long long rdtsc(void)
 {
 	unsigned int lo, hi;
 	unsigned int id;
 
-	asm volatile ("rdtscp" : "=a"(lo), "=c"(id), "=d"(hi) :: "memory");
+	asm volatile ("rdtscp" : "=a"(lo), "=c"(id), "=d"(hi));
 
 	return ((unsigned long long)hi << 32ULL | (unsigned long long)lo);
 }
-#endif
 
 int main(int argc, char** argv)
 {