- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b79bf0b1-5d51-4e45-a5c0-fa0955e85c04
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 747abb19-aedb-44a6-8ba8-36accb4e3da5
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2aff6cc8-c32f-4e6c-bea1-3c5e63631ec9
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok
      == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b22fe40-6c3f-443e-abde-1b065261ce9a
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (pmutex_adutux_mutex_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088f4ffd-6db8-4f18-8daf-b4b94985d412
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (pmutex_adutux_mutex_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc7bcd23-df10-420c-ade3-e752825777d1
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (pmutex_adutux_mutex_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26a4ebe1-1d4a-4a62-95c9-8342fe440109
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (smutex_buflock_of_adu_device_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6147155d-685b-493a-993e-93c74e254799
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (smutex_buflock_of_adu_device_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83af48fe-6f94-4cd8-b06a-ebd527964004
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (smutex_buflock_of_adu_device_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f451155-219b-4d78-a416-70aa78c1b6a0
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (pmutex_mtx_of_adu_device_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdb783c9-70b3-4328-9731-2d7369259439
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (pmutex_mtx_of_adu_device_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86aee59a-d91e-417a-a89f-0b1538d09786
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (pmutex_mtx_of_adu_device_locked || ((((((((((((((unsigned
      char )__mod_usb_device_table.bDeviceClass == (unsigned char)0 && (unsigned char
      )__mod_usb_device_table.bDeviceProtocol == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bDeviceSubClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceClass == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceNumber == (unsigned char)0) && (unsigned char
      )__mod_usb_device_table.bInterfaceProtocol == (unsigned char)0) && (unsigned
      char )__mod_usb_device_table.bInterfaceSubClass == (unsigned char)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_hi == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.bcdDevice_lo == (unsigned short)0) && (unsigned
      short )__mod_usb_device_table.idProduct == (unsigned short)0) && (unsigned short
      )__mod_usb_device_table.idVendor == (unsigned short)0) && (unsigned short )__mod_usb_device_table.match_flags
      == (unsigned short)0) && (unsigned long )__mod_usb_device_table.driver_info
      == 0UL) && (__this_module.sig_ok == (_Bool)0 || __this_module.sig_ok == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de4b7e31-52c7-4784-b5c6-800595d263a3
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5958
    column: 3
    function: ldv_dispatch_default_register_3_4_4
  location_invariant:
    string: '! multithreaded || (((((((((((((unsigned char )__mod_usb_device_table.bDeviceClass
      == (unsigned char)0 && (unsigned char )__mod_usb_device_table.bDeviceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bDeviceSubClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceNumber
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceSubClass
      == (unsigned char)0) && (unsigned short )__mod_usb_device_table.bcdDevice_hi
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.bcdDevice_lo
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.idProduct ==
      (unsigned short)0) && (unsigned short )__mod_usb_device_table.idVendor == (unsigned
      short)0) && (unsigned short )__mod_usb_device_table.match_flags == (unsigned
      short)0) && (unsigned long )__mod_usb_device_table.driver_info == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f082140-0b45-4ed0-a709-9882a1f6de17
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5996
    column: 3
    function: ldv_dispatch_insmod_register_7_3
  location_invariant:
    string: '! multithreaded || (((((((((((((unsigned char )__mod_usb_device_table.bDeviceClass
      == (unsigned char)0 && (unsigned char )__mod_usb_device_table.bDeviceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bDeviceSubClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceNumber
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceSubClass
      == (unsigned char)0) && (unsigned short )__mod_usb_device_table.bcdDevice_hi
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.bcdDevice_lo
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.idProduct ==
      (unsigned short)0) && (unsigned short )__mod_usb_device_table.idVendor == (unsigned
      short)0) && (unsigned short )__mod_usb_device_table.match_flags == (unsigned
      short)0) && (unsigned long )__mod_usb_device_table.driver_info == 0UL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7dbb3ddd-1b88-4929-874e-b0f0bc4cb1c2
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6013
    column: 3
    function: ldv_dispatch_register_6_3
  location_invariant:
    string: '! multithreaded || (((((((((((((unsigned char )__mod_usb_device_table.bDeviceClass
      == (unsigned char)0 && (unsigned char )__mod_usb_device_table.bDeviceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bDeviceSubClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceClass
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceNumber
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceProtocol
      == (unsigned char)0) && (unsigned char )__mod_usb_device_table.bInterfaceSubClass
      == (unsigned char)0) && (unsigned short )__mod_usb_device_table.bcdDevice_hi
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.bcdDevice_lo
      == (unsigned short)0) && (unsigned short )__mod_usb_device_table.idProduct ==
      (unsigned short)0) && (unsigned short )__mod_usb_device_table.idVendor == (unsigned
      short)0) && (unsigned short )__mod_usb_device_table.match_flags == (unsigned
      short)0) && (unsigned long )__mod_usb_device_table.driver_info == 0UL)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5e933709-b3c9-4f73-abd0-4f1c60f57e8b
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 831c461f-9794-4de3-9153-9b73b384d83a
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7123
    column: 5
    function: ldv_mutex_lock_interruptible_or_killable_mtx_of_adu_device
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f8cdca27-b4d9-4667-8190-5a6215a64a2e
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7109
    column: 3
    function: ldv_mutex_lock_mtx_of_adu_device
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: fc52c91f-78b5-4a00-9f76-30a6312edca5
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_buflock_of_adu_device_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fd5c47d8-dcd8-4c47-8d32-f8e1c671975d
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_buflock_of_adu_device_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7372
    column: 3
    function: ldv_spin_lock_buflock_of_adu_device
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe399c1d-f664-478d-b536-a0e58b6bf839
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_buflock_of_adu_device_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7381
    column: 3
    function: ldv_spin_unlock_buflock_of_adu_device
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b08666dd-2fab-4318-ac93-b02138754341
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4049a54f-d90f-44ea-9ebd-71e731513f2d
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5994
    column: 3
    function: ldv_dispatch_insmod_register_7_3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: bce94fc5-6e51-4f49-82c6-65e7327d4df4
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b39161b-1011-463e-a8ad-285a92ed4e52
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6951
    column: 3
    function: ldv_mutex_unlock_adutux_mutex
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a77d15f-06cc-4a26-9e99-0765d4f007cd
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6901
    column: 5
    function: ldv_mutex_lock_interruptible_or_killable_adutux_mutex
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 39949a42-c15a-4d5e-b34f-409bef9fa8d7
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_mtx_of_adu_device_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 7173
    column: 3
    function: ldv_mutex_unlock_mtx_of_adu_device
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ff6e595f-3d01-444a-bdf4-0730e79d092c
    creation_time: 2024-04-26T10:46:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: pmutex_adutux_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 6887
    column: 3
    function: ldv_mutex_lock_adutux_mutex
