- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afb590e6-d449-4426-b8a0-7fb77de48c06
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 860dc40d-33ca-4439-af24-a6c05c3cbc2f
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 0b468c12-efde-4ce1-9194-50820d395e93
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 3f92c1c3-6c3b-4df0-b05a-32e927d8f70d
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 03cecd58-53b3-471d-b0cd-679938aa3eab
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 1514ad5d-7695-4365-aeee-af81a367c58a
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 1737aa7c-d246-4565-8c6e-d0e8c500e562
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 8b83c029-2807-4d66-b95b-2cf1d7004b0a
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: e8a6a513-c1c3-46ab-803d-2cc349543431
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: c3f03d91-e842-4d2a-bb11-ce6bb94660e2
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 3a4e031b-dbd1-45f5-b61b-46b027ff6247
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: eb609511-e9f6-4a97-9c16-15146c9417aa
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 4698641e-6a74-4daa-84f6-ec2bcb0c88f5
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: f1a8f59f-729f-4f12-9ebd-57f56865346b
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 53ff9d16-44f1-4f96-8db5-aaae4978a664
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 6ef6c686-c498-478d-94c9-8191bfad81b2
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 6d7e0661-33dc-4474-b757-c78fdc150fcf
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 749ca3f9-69b9-434a-8fb0-cbd306ac259a
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 0b5c060c-851b-47e4-9224-af62d53c0b48
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: c8a5ce5c-da6f-4704-b660-3737dda91f91
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 92c5e072-dfbd-4d1f-b3db-ada835169169
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: db4a0485-e87a-4c09-a92a-c99a22d413d2
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: f071fc1a-b084-49e1-aa85-afcb15d0905e
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 723ee555-6a67-46e3-bba3-f18d1fe5be8f
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 4a973f52-0b70-4a20-b3ae-1ba2f8b60df8
    creation_time: 2024-06-19T11:49:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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
