5448 {
5449#line 726
5450 pca_func(var_group1);
5451 }
5452#line 733
5453 goto switch_break;
5454 switch_default:
5455#line 734
5456 goto switch_break;
5457 } else {
5458 switch_break: ;
5459 }
5460 }
5461 }
5462 }
5463 while_break: ;
5464 }
5465 {
5466#line 743
5467 ldv_check_final_state();
5468 }
5469#line 746
5470 return;
5471}
5472}
5473#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/250/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5474void ldv_blast_assert(void)
5475{
5476
5477 {
5478 ERROR:
5479#line 6
5480 goto ERROR;
5481}
5482}
5483#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/250/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5484extern int __VERIFIER_nondet_int(void) ;
5485#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/250/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5486int ldv_mutex = 1;
5487#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/250/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5488int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )