Small bugfixes

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 */