6039 {
6040#line 236
6041 drm_usb_set_busid(var_group1, var_group2);
6042 }
6043#line 243
6044 goto switch_break;
6045 switch_default:
6046#line 244
6047 goto switch_break;
6048 } else {
6049 switch_break: ;
6050 }
6051 }
6052 }
6053 }
6054 while_break: ;
6055 }
6056 {
6057#line 253
6058 ldv_check_final_state();
6059 }
6060#line 256
6061 return;
6062}
6063}
6064#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6961/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6065void ldv_blast_assert(void)
6066{
6067
6068 {
6069 ERROR:
6070#line 6
6071 goto ERROR;
6072}
6073}
6074#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6961/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6075extern int __VERIFIER_nondet_int(void) ;
6076#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6961/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6077int ldv_mutex = 1;
6078#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6961/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6079int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )