40};
41#line 1 "scenario.o"
42#pragma merger(0,"scenario.i","")
43#line 2 "scenario.c"
44void bigMacCall(void) ;
45#line 3
46void cleanup(void) ;
47#line 1 "scenario.c"
48void test(void)
49{
50
51 {
52 {
53#line 2
54 bigMacCall();
55#line 3
56 cleanup();
57 }
58#line 53 "scenario.c"
59 return;
60}
61}
62#line 1 "wsllib_check.o"
63#pragma merger(0,"wsllib_check.i","")
64#line 3 "wsllib_check.c"
65void __automaton_fail(void)
66{
67
68 {
69 goto ERROR;
70 ERROR: ;
71#line 53 "wsllib_check.c"
72 return;
73}
74}
75#line 1 "Specification9_spec.o"
76#pragma merger(0,"Specification9_spec.i","")
77#line 26 "Elevator.h"
78int isEmpty(void) ;
79#line 38
80int areDoorsOpen(void) ;