ClabureDB: Classified Bug-Reports Database

                         }
                       }
                     }
                   }
                 }
               }
             }
           }
         }
       }
     }
   }
   while_0_break: /* CIL Label */ ;
   }
   {
 #line 60
   bobToRjh();
   }
 #line 167 "scenario.c"
   return;
 }
 }
 #line 1 "wsllib_check.o"
 #pragma merger(0,"wsllib_check.i","")
 #line 3 "wsllib_check.c"
 void __automaton_fail(void) 
 { 
 
   {
   goto ERROR;
   ERROR: ;
 #line 53 "wsllib_check.c"
   return;
 }
 }
 #line 1 "Client.o"
 #pragma merger(0,"Client.i","")
 #line 359 "/usr/include/stdio.h"
 extern int printf(char const   * __restrict  __format  , ...) ;
 #line 688
 extern int puts(char const   *__s ) ;