671 }
672 }
673#line 903 "libacc.c"
674 __cil_tmp7 = i - 1;
675#line 903
676 __cil_tmp8 = (unsigned long )this;
677#line 903
678 __cil_tmp9 = __cil_tmp8 + 24;
679#line 903
680 mem_13 = (char const ***)__cil_tmp9;
681#line 903
682 __cil_tmp10 = *mem_13;
683#line 903
684 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
685#line 903
686 retValue_acc = *__cil_tmp11;
687#line 905
688 return (retValue_acc);
689#line 912
690 return (retValue_acc);
691}
692}
693#line 1 "wsllib_check.o"
694#pragma merger(0,"wsllib_check.i","")
695#line 3 "wsllib_check.c"
696void __automaton_fail(void)
697{
698
699 {
700 goto ERROR;
701 ERROR: ;
702#line 53 "wsllib_check.c"
703 return;
704}
705}
706#line 1 "Specification4_spec.o"
707#pragma merger(0,"Specification4_spec.i","")
708#line 10 "MinePump.h"
709int isPumpRunning(void) ;
710#line 11 "Specification4_spec.c"
711__inline void __utac_acc__Specification4_spec__1(void)