diff --git a/src/main.c b/src/main.c
index 5769321afde8266283c5fad91d93044191021993..83de52d4897f8561a99e95aaac4b2880210196b9 100644
--- a/src/main.c
+++ b/src/main.c
@@ -42,6 +42,12 @@
 #define r1_Ceiling 2
 #define r2_Ceiling 1
 
+// Analysis variables
+static volatile int state;
+#ifdef KLEE
+static int job;
+#endif
+
 void work(int i) {
 	volatile int k = 0;
 	for (int j = 0; j < 100 * i; j++) {
@@ -90,8 +96,6 @@ TASK(j3) {
 
 #ifdef KLEE
 /* The case when KLEE makes the path analysis */
-static int state;
-static int job;
 
 int main() {
 	klee_make_symbolic(&job, sizeof(job), "job");
@@ -113,6 +117,7 @@ int main() {
 		EXTI3_IRQHandler();
 		break;
 	}
+}
 
 #elif defined KLEE_WCET
 /* The case when gdb runs WCET benchmarking */