- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f68b37f-98b5-4c24-86b5-55eb89b4b335
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eacbe865-8875-4459-8cc0-d96124fdf76f
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a1fcb8e-2984-42fb-8441-290de9b9c9b6
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1813f5c1-eccb-4c6b-b6eb-12ff6048bff2
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 2b4f76f1-c6a2-4848-b0d4-7221eccce64c
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: ea6dd4cb-e2d7-49ef-902f-a663d647a252
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7761c3fe-da24-427a-ad8d-d74161a2eaf3
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6af0551d-9a6f-4f4f-9c1d-5d1a7a4c9c2d
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e2b1e31-ef12-477e-8815-42582e6accaf
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2a5e907-db9b-4fdc-ac01-17e4d9e7c443
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5afc77b1-3fbf-49bf-af30-5e7098ab7952
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bb5a14b-068a-4cf2-9097-2de5b95a0b0c
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8a1ebdde-e938-485d-9e9b-fedbb1d42dd1
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 2213b5f9-19da-4e16-b3dc-98620617e630
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: ecfe54a7-6c8c-4157-a0af-0e02eee3c926
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: b1b16529-df4f-4698-9a6f-653507a61aeb
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: dfb33452-90c6-4eb7-ba93-6139f9cfddad
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 4ffc8054-02c8-4173-a72f-1c5f0a0324b6
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: acd672ba-1be6-40bf-9219-0183b40d42ba
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 4e1d61a1-3e14-4e4f-a09d-eac847ba8040
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 1edc77fe-b7ef-4923-9677-7d7b29c04f13
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 9a093da9-9d6d-4aa4-8d2b-c583453665ca
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: 0b207436-146b-4213-8edd-ede4a5a6732b
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: f96b8178-fcb0-4036-98ae-7987a490d832
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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: bf0f7e30-c269-4fc6-9fa4-03134110e624
    creation_time: 2024-04-30T10:03:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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
