7292 {
7293#line 301
7294 vp3054_bit_getscl(var_vp3054_bit_getscl_2_p0);
7295 }
7296#line 308
7297 goto switch_break;
7298 switch_default:
7299#line 309
7300 goto switch_break;
7301 } else {
7302 switch_break: ;
7303 }
7304 }
7305 }
7306 }
7307 while_break: ;
7308 }
7309 {
7310#line 318
7311 ldv_check_final_state();
7312 }
7313#line 321
7314 return;
7315}
7316}
7317#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14482/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7318void ldv_blast_assert(void)
7319{
7320
7321 {
7322 ERROR:
7323#line 6
7324 goto ERROR;
7325}
7326}
7327#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14482/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7328extern int __VERIFIER_nondet_int(void) ;
7329#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14482/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7330int ldv_mutex = 1;
7331#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14482/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7332int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )