ClabureDB: Classified Bug-Reports Database

                        }
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  while_0_break: /* CIL Label */ ;
  }
  {
#line 53
  bobToRjh();
  }
#line 153 "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 "libacc.o"
#pragma merger(0,"libacc.i","")
#line 73 "/usr/include/assert.h"
extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
                                                                      char const   *__file ,
                                                                      unsigned int __line ,