6265 {
6266#line 255
6267 pl_reset(var_group1);
6268 }
6269#line 262
6270 goto switch_break;
6271 switch_default:
6272#line 263
6273 goto switch_break;
6274 } else {
6275 switch_break: ;
6276 }
6277 }
6278 }
6279 }
6280 while_break: ;
6281 }
6282 {
6283#line 272
6284 ldv_check_final_state();
6285 }
6286#line 275
6287 return;
6288}
6289}
6290#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9624/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6291void ldv_blast_assert(void)
6292{
6293
6294 {
6295 ERROR:
6296#line 6
6297 goto ERROR;
6298}
6299}
6300#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9624/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6301extern int __VERIFIER_nondet_int(void) ;
6302#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9624/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6303int ldv_mutex = 1;
6304#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9624/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6305int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )