6724 switch_default:
6725#line 1036
6726 goto switch_break;
6727 } else {
6728 switch_break: ;
6729 }
6730 }
6731 }
6732 }
6733 while_break: ;
6734 }
6735 ldv_module_exit:
6736 {
6737#line 1067
6738 wacom_exit();
6739 }
6740 ldv_final:
6741 {
6742#line 1070
6743 ldv_check_final_state();
6744 }
6745#line 1073
6746 return;
6747}
6748}
6749#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6750void ldv_blast_assert(void)
6751{
6752
6753 {
6754 ERROR:
6755#line 6
6756 goto ERROR;
6757}
6758}
6759#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6760extern int __VERIFIER_nondet_int(void) ;
6761#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6762int ldv_mutex = 1;
6763#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/235/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6764int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )