- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2c69924-18d6-4319-b65e-5c4456825370
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 0d32ec1d-b22e-4c25-8ba8-e560bce50ee9
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: fbfe26ae-4384-4332-bb90-f29a1eccb700
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: df081acc-f293-4c19-975b-cae708799eaf
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: d1923632-33ff-47e0-9be3-b8b6cb14fa51
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 4a19a75d-e85e-4009-87ba-18ddbd325536
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 7173c1b2-1312-4361-91a6-1ff3af0064e9
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: deaba294-c362-4d09-9f2a-dea1de54fdf2
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: beba54c9-bf6f-4102-b5ae-b288f24ad180
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 482c48ec-d1df-48f7-a032-564ab89f11ab
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: e9ffc6e5-05df-4132-9d43-de91571b6c42
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: c618c27f-317d-4c5f-9646-bb49109b212e
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 74687574-25f0-47d2-aebb-f7d56205f598
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 4ee8428d-ef26-47c3-a953-558f48aa45df
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: dafb2d90-ade8-4cdb-991a-3ae8b62b1fa2
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 9d132869-5f47-42d9-a4b5-98a1fe6a3d0a
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 57c42536-e825-46ef-a8bf-f7070111e68d
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: d0b55769-2cd4-42e8-8dd7-9c45f6bbc8f9
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 00da84f6-2bd8-447a-874f-ce7d9a4cbe55
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: ab535417-a8b2-4aa5-bc9d-d94946a061c9
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 8a0b5cc2-cd0d-4677-ade0-3e2cd3d9ed61
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 1aa2d592-1907-43a5-a0a2-25620db40a41
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 0e238ab8-f5a2-4d8a-9c2e-e13dd092282f
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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: 4df61937-db47-4e2e-81e8-cbb03aa2398f
    creation_time: 2023-02-02T14:22:40Z
    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''
        ''protection-read'' ''--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
