diff --git a/include/SRP_wcet.h b/include/SRP_wcet.h
index 609d5ef522f297966acd8170d4eb0978e5bbd331..889458382b1aaa7969d266186fd3ffcd809b7d36 100644
--- a/include/SRP_wcet.h
+++ b/include/SRP_wcet.h
@@ -66,5 +66,3 @@ locks eventlist[MAX_NUM_LOCKS];
 #define BREAKPOINT
 
 void finish_execution(void) {}
-//void terminate_execution(void) {}
-
diff --git a/klee_stm_gdb.py b/klee_stm_gdb.py
index f6ab1c52fd10cc7a74daad53f9ecd3a3bcdb822d..d59e0568bbbdf6e364be3094fb05af7091b4f722 100644
--- a/klee_stm_gdb.py
+++ b/klee_stm_gdb.py
@@ -33,7 +33,7 @@ cur.execute('''CREATE TABLE IF NOT EXISTS events
     FILE           TEXT     NOT NULL,
     TIME           INT      NOT NULL,
     RESOURCE       TEXT     NOT NULL,
-    ACTION         TEXT
+    ACTION         TEXT,
     JOB            TEXT);''')
 
 
diff --git a/src/main.c b/src/main.c
index 83de52d4897f8561a99e95aaac4b2880210196b9..c2ccd95f6fa4e72e29a7a6c0d09cbc2021758ec2 100644
--- a/src/main.c
+++ b/src/main.c
@@ -44,9 +44,7 @@
 
 // Analysis variables
 static volatile int state;
-#ifdef KLEE
 static int job;
-#endif
 
 void work(int i) {
 	volatile int k = 0;
@@ -100,9 +98,13 @@ TASK(j3) {
 int main() {
 	klee_make_symbolic(&job, sizeof(job), "job");
 
+	klee_assume(job > 0 && job < 4);
+
 	switch (job) {
-		case 1:
+        default:
+        klee_make_symbolic(&state, sizeof(state), "state");
 		// check task 1
+        case 1:
 		klee_make_symbolic(&state, sizeof(state), "state");
 		EXTI1_IRQHandler();
 		break;
@@ -116,12 +118,13 @@ int main() {
 		klee_make_symbolic(&state, sizeof(state), "state");
 		EXTI3_IRQHandler();
 		break;
+            /*klee_make_symbolic(&state, sizeof(state), "state");*/
+            /*break;*/
 	}
 }
 
 #elif defined KLEE_WCET
 /* The case when gdb runs WCET benchmarking */
-static int state;
 static int job;
 int main() {