diff --git a/include/SRP_wcet.h b/include/SRP_wcet.h
index b8c1182621e48ff87e21a7c30d1f1d09e79b629a..787cea218a03e4944f317dc413cc38d513ab6035 100644
--- a/include/SRP_wcet.h
+++ b/include/SRP_wcet.h
@@ -44,14 +44,15 @@ typedef struct locks
 
 } locks;
 
-uint32_t event_count = 0;
 
-#define MAX_NUM_LOCKS 10
+
+int event_count = 0;
 
 /* Create array containing structs of type locks */
+#define MAX_NUM_LOCKS 10
 locks eventlist[MAX_NUM_LOCKS];
-//#define TRACE_EVENT(event, el)({eventlist[event_count].time = DWT->CYCCNT; eventlist[event_count].action = event; eventlist[event_count].elem = el; event_count+=1;})
-#define TRACE_EVENT(event, el)({})
+
+#define TRACE_EVENT(event, el)({eventlist[event_count].time = DWT->CYCCNT; eventlist[event_count].action = event; eventlist[event_count].elem = el; event_count+=1;})
 
 
 // #define Ceiling(R)		(R##_Ceiling)
@@ -64,8 +65,8 @@ locks eventlist[MAX_NUM_LOCKS];
 // #define BARRIER_UNLOCK 	{ }
 #define JOB_REQUEST(J)	{ }
 
-#define LOCK(R) 		TRACE_EVENT(L, #R);
-#define UNLOCK(R) 		TRACE_EVENT(R, #R);
+#define LOCK(X) 		TRACE_EVENT(L, X);
+#define UNLOCK(X) 		TRACE_EVENT(R, X);
 
 // #define SETPRIO(J)		{ }
 // #define ENABLE(J)		{ }
diff --git a/src/main.c b/src/main.c
index 8c06bb9c4bb4620f88269350044cbe9d1789c4db..dabf3bba3c4669b7e8c25081d702d77bf6264ece 100644
--- a/src/main.c
+++ b/src/main.c
@@ -31,88 +31,99 @@
 
 static int state;
 
-void work(int i) {
-	volatile int k =0;
-	for (int j =0; j < 100 * i; j++)
-		k++;
+void work(int i)
+{
+    volatile int k =0;
+    for (int j =0; j < 100 * i; j++)
+    {
+        k++;
+    }
 }
 
-TASK(j1) {
-	LOCK(r2);
+TASK(j1)
+{
+    LOCK(r2);
 
-		JOB_REQUEST(j2); 			// job execution request for j2
+    JOB_REQUEST(j2); 			// job execution request for j2
 
-		if (state > 0)
-			work(10);
-		else
-			work(5);
+    if (state > 0)
+    {
+        work(10);
+    }
+    else
+    {
+        work(5);
+    }
 
-		/*
-		LOCK(r1);
+    LOCK(r1);
 #ifdef enable_itm
-			trace_printf("j1_r1_locked, before job request j2\n");
+    trace_printf("j1_r1_locked, before job request j2\n");
 #endif
-			JOB_REQUEST(j2);
+    JOB_REQUEST(j2);
 #ifdef enable_itm
-			trace_printf("j1_r1_locked, after job request j2\n");
+    trace_printf("j1_r1_locked, after job request j2\n");
 #endif
-		UNLOCK(r1);
-		*/
-	UNLOCK(r2);
+    UNLOCK(r1);
+    UNLOCK(r2);
 }
 
-TASK(j2) {
+TASK(j2)
+{
 #ifdef enable_itm
-	trace_printf("j2_enter\n");
+    trace_printf("j2_enter\n");
 #endif
-	LOCK(r1);
+    LOCK(r1);
 #ifdef enable_itm
-		trace_printf("j2_r1_locked\n");
+    trace_printf("j2_r1_locked\n");
 #endif
-	UNLOCK(r1);
+    UNLOCK(r1);
 #ifdef enable_itm
-	trace_printf("j2_exit\n");
+    trace_printf("j2_exit\n");
 #endif
 }
 
-int main() {
+int main()
+{
 #ifdef enable_itm
-	trace_printf("\nInit\n");
+    trace_printf("\nInit\n");
 #endif
 
 #ifndef KLEE
 
-	#ifndef KLEE_WCET
-	SETPRIO(j1);				// Set HW priorities
-	SETPRIO(j2);
-	SETPRIO(j3);
-	ENABLE(j1);					// Enable HW sources
-	ENABLE(j2);
-	ENABLE(j3);
-
-	JOB_REQUEST(j1);			// comment out in assignment c
-	//JOB_REQUEST(j3);  		// use in assignment c
-
-	BREAKPOINT;
-	while (1) ;
-	return 0;
-	#else
-	dwt_enable();
-	DWT->CYCCNT = 0;
-
-	event_count = 0;
-	TRACE_EVENT(S, j1);
-	EXTI1_IRQHandler();
-	TRACE_EVENT(E, j1);
-	finish_execution();
-	terminate_execution();
-	#endif
+    dwt_enable();
+    DWT->CYCCNT = 0;
+#ifndef KLEE_WCET
+
+    SETPRIO(j1);				// Set HW priorities
+    SETPRIO(j2);
+    SETPRIO(j3);
+    ENABLE(j1);					// Enable HW sources
+    ENABLE(j2);
+    ENABLE(j3);
+
+    JOB_REQUEST(j1);			// comment out in assignment c
+    //JOB_REQUEST(j3);  		// use in assignment c
+
+    BREAKPOINT;
+    while (1) ;
+    return 0;
+
+    /* The case when NOT running WCET benchmark nor KLEE-analysis */
+#else
+
+    TRACE_EVENT(S, j1);
+    EXTI1_IRQHandler();
+    TRACE_EVENT(E, j1);
+#endif
+
+    finish_execution();
+    terminate_execution();
 
 #elif (JOB == 1)
-	// check task 1
-	klee_make_symbolic(&state, sizeof(state), "state");
-	//IRQh(j1);
-	EXTI1_IRQHandler();
+    // check task 1
+    klee_make_symbolic(&state, sizeof(state), "state");
+    //IRQh(j1);
+    EXTI1_IRQHandler();
 
 #endif
 }