diff --git a/src/main.c b/src/main.c
index c2ccd95f6fa4e72e29a7a6c0d09cbc2021758ec2..8a59cd772bd0ccecdc59217100c6ba96f34bdc5e 100644
--- a/src/main.c
+++ b/src/main.c
@@ -46,132 +46,142 @@
 static volatile int state;
 static int job;
 
-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) {
-	TRACE("j1_enter\n");
-	LOCK(r2);
-	JOB_REQUEST(j2); 			// job execution request for j2
-
-	if (state > 0) {
-		work(10);
-	} else {
-		work(5);
-	}
-
-	LOCK(r1);
-	TRACE("j1_r1_locked, before job request j2\n");
-
-	JOB_REQUEST(j2);
-	TRACE("j1_r1_locked, after job request j2\n");
-	UNLOCK(r1);
-	UNLOCK(r2);
+TASK(j1)
+{
+    TRACE("j1_enter\n");
+    LOCK(r2);
+    JOB_REQUEST(j2); 			// job execution request for j2
+
+    if (state > 0)
+    {
+        work(10);
+    }
+    else
+    {
+        work(5);
+    }
+
+    LOCK(r1);
+    TRACE("j1_r1_locked, before job request j2\n");
+
+    JOB_REQUEST(j2);
+    TRACE("j1_r1_locked, after job request j2\n");
+    UNLOCK(r1);
+    UNLOCK(r2);
 }
 
-TASK(j2) {
-	TRACE("j2_enter\n");
-	LOCK(r1);
-	TRACE("j2_r1_locked\n");
-	work(5);
-	UNLOCK(r1);
-	TRACE("j2_exit\n");
+TASK(j2)
+{
+    TRACE("j2_enter\n");
+    LOCK(r1);
+    TRACE("j2_r1_locked\n");
+    work(5);
+    UNLOCK(r1);
+    TRACE("j2_exit\n");
 }
 
-TASK(j3) {
-	TRACE("j3_enter\n");
-	LOCK(r1);
-	TRACE("j3_r1_locked\n");
-	work(1);
-	UNLOCK(r1);
-	JOB_REQUEST(j1);
-	TRACE("j3_exit\n");
+TASK(j3)
+{
+    TRACE("j3_enter\n");
+    LOCK(r1);
+    TRACE("j3_r1_locked\n");
+    work(1);
+    UNLOCK(r1);
+    JOB_REQUEST(j1);
+    TRACE("j3_exit\n");
 }
 
 #ifdef KLEE
 /* The case when KLEE makes the path analysis */
 
-int main() {
-	klee_make_symbolic(&job, sizeof(job), "job");
+int main()
+{
+    klee_make_symbolic(&job, sizeof(job), "job");
 
-	klee_assume(job > 0 && job < 4);
+    klee_assume(job > 0 && job < 4);
 
-	switch (job) {
-        default:
+    switch (job)
+    {
+    default:
+        klee_make_symbolic(&state, sizeof(state), "state");
+    // check task 1
+    case 1:
+        klee_make_symbolic(&state, sizeof(state), "state");
+        EXTI1_IRQHandler();
+        break;
+    case 2:
+        // check task 2
+        klee_make_symbolic(&state, sizeof(state), "state");
+        EXTI2_IRQHandler();
+        break;
+    case 3:
+        // check task 3
         klee_make_symbolic(&state, sizeof(state), "state");
-		// check task 1
-        case 1:
-		klee_make_symbolic(&state, sizeof(state), "state");
-		EXTI1_IRQHandler();
-		break;
-		case 2:
-		// check task 2
-		klee_make_symbolic(&state, sizeof(state), "state");
-		EXTI2_IRQHandler();
-		break;
-		case 3:
-		// check task 3
-		klee_make_symbolic(&state, sizeof(state), "state");
-		EXTI3_IRQHandler();
-		break;
-            /*klee_make_symbolic(&state, sizeof(state), "state");*/
-            /*break;*/
-	}
+        EXTI3_IRQHandler();
+        break;
+    }
 }
 
 #elif defined KLEE_WCET
 /* The case when gdb runs WCET benchmarking */
 static int job;
-int main() {
-
-	dwt_enable();
-	DWT->CYCCNT = 0;
-
-	switch (job) {
-	case 1:
-		TRACE_EVENT(S, j1);
-		EXTI1_IRQHandler();
-		TRACE_EVENT(E, j1);
-		break;
-	case 2:
-		TRACE_EVENT(S, j2);
-		EXTI2_IRQHandler();
-		TRACE_EVENT(E, j2);
-		break;
-	case 3:
-		TRACE_EVENT(S, j3);
-		EXTI3_IRQHandler();
-		TRACE_EVENT(E, j3);
-		break;
-	}
-
-	finish_execution();			// gdb breakpoint
-	// terminate_execution();
+int main()
+{
+
+    dwt_enable();
+    DWT->CYCCNT = 0;
+
+    switch (job)
+    {
+    case 1:
+        TRACE_EVENT(S, j1);
+        EXTI1_IRQHandler();
+        TRACE_EVENT(E, j1);
+        break;
+    case 2:
+        TRACE_EVENT(S, j2);
+        EXTI2_IRQHandler();
+        TRACE_EVENT(E, j2);
+        break;
+    case 3:
+        TRACE_EVENT(S, j3);
+        EXTI3_IRQHandler();
+        TRACE_EVENT(E, j3);
+        break;
+    }
+
+    finish_execution();			// gdb breakpoint
 }
 
 #else
 // this will be run in the production code
-int main() {
-	TRACE("\nInit\n");
-	SETPRIO(j1);				// Set HW priorities
-	SETPRIO(j2);
-	SETPRIO(j3);
-	ENABLE(j1);// Enable HW sources
-	ENABLE(j2);
-	ENABLE(j3);
-
-	JOB_REQUEST(j3);// use in assignment c
-
-	BREAKPOINT
-	;
-
-	while (1)
-	;
-	return 0;
+int main()
+{
+    TRACE("\nInit\n");
+    SETPRIO(j1);				// Set HW priorities
+    SETPRIO(j2);
+    SETPRIO(j3);
+    ENABLE(j1);// Enable HW sources
+    ENABLE(j2);
+    ENABLE(j3);
+
+    JOB_REQUEST(j3);// use in assignment c
+
+    BREAKPOINT
+    ;
+
+    while (1)
+        ;
+    return 0;
 }
 #endif