3173 goto switch_break;
3174 switch_default:
3175#line 241
3176 goto switch_break;
3177 } else {
3178 switch_break: ;
3179 }
3180 }
3181 }
3182 }
3183 while_break: ;
3184 }
3185 {
3186#line 256
3187 gyration_exit();
3188 }
3189 ldv_final:
3190 {
3191#line 259
3192 ldv_check_final_state();
3193 }
3194#line 262
3195 return;
3196}
3197}
3198#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/197/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3199void ldv_blast_assert(void)
3200{
3201
3202 {
3203 ERROR:
3204#line 6
3205 goto ERROR;
3206}
3207}
3208#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/197/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3209extern int __VERIFIER_nondet_int(void) ;
3210#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/197/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3211int ldv_mutex = 1;
3212#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/197/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3213int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )