- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 024cb993-d7ed-4468-8105-28d2a5b78ad5
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  location_invariant:
    string: -128 <= ldv_2_ret_default
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19b6d3cb-2707-49fa-ba07-d924cd29976f
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  location_invariant:
    string: -19 <= ldv_2_ret_default
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7350efc3-69a4-497e-ae07-ff3da3d45c45
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  location_invariant:
    string: ldv_2_ret_default <= 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2012b18-f23a-4ad7-9c90-f89f41115553
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  location_invariant:
    string: ldv_2_ret_default <= 127
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5de0b094-e527-4b2a-89a5-5b86c3bb5498
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  location_invariant:
    string: 0 <= should_submit
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f1d6aaa-6e7f-41a8-a481-0d46b24c1733
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  location_invariant:
    string: 1U <= count
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 881c5d0e-a49e-48df-9346-eb4fccaf4cd8
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  location_invariant:
    string: should_submit <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8257dfe8-7968-4715-a74b-50051e22edf0
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  location_invariant:
    string: count != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3c57edf-08ec-4dbe-9cf8-8e8fdce1faa8
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  location_invariant:
    string: timeout != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f6cd472-a776-45f5-b1de-47e4f05995e6
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5364
    column: 6
    function: adu_write
  location_invariant:
    string: 0 <= retval
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a121c404-5561-4fff-88f2-fba07138f3bd
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5470
    column: 6
    function: adu_probe
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62e467f0-f457-4612-8274-a76c27c5e487
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5470
    column: 6
    function: adu_probe
  location_invariant:
    string: i <= 255
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 33e95367-4464-4ef5-b3ab-77031415d93b
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  loop_invariant:
    string: -128 <= ldv_2_ret_default
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b3286659-c183-4451-8681-6741ee245763
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  loop_invariant:
    string: -19 <= ldv_2_ret_default
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d9f271c8-b7b9-4ab8-ba99-e4543aa0d92f
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  loop_invariant:
    string: ldv_2_ret_default <= 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 59897128-52fc-4ca0-be4c-d276a2033589
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5809
    column: 2
    function: ldv_character_driver_scenario_2
  loop_invariant:
    string: ldv_2_ret_default <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1404544b-9043-47be-93d6-6e45a548b4a4
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  loop_invariant:
    string: 0 <= should_submit
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ddabf74-8806-4cc6-9a3b-436d4057b4ff
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  loop_invariant:
    string: 1U <= count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bdfb016-63bc-486d-958f-b4fbc999e704
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  loop_invariant:
    string: should_submit <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 84018884-3152-4009-91ba-12d25d492497
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  loop_invariant:
    string: count != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eecf8341-9ae8-44b5-bc96-01a98a3eee20
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 4922
    column: 6
    function: adu_read
  loop_invariant:
    string: timeout != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c51806c-ded2-4723-9545-f84fbe0a5c60
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5364
    column: 6
    function: adu_write
  loop_invariant:
    string: 0 <= retval
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a86d7007-f9ab-465e-8904-eb22fe33362d
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5470
    column: 6
    function: adu_probe
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ef8d0ced-1e24-4e60-8f34-7ecf4f58357c
    creation_time: 2023-02-02T14:23:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--usb--misc--adutux.ko.cil.i
    file_hash: d21289ad0260bc29d79b2bd61c2535ad4b8522ed30b4caa2844d314826a0bd1c
    line: 5470
    column: 6
    function: adu_probe
  loop_invariant:
    string: i <= 255
    type: assertion
    format: C
