- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e96b620-6836-42b6-894c-15845b278265
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6257
    column: 6
    function: w83977af_init
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0742f4b3-5872-4956-80d3-4a27d2125fdd
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6285
    column: 6
    function: w83977af_cleanup
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50557543-8db4-44d8-8d5c-211e9734cf50
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: 0 <= irq___0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76684757-02af-4ee1-a9eb-f373d3e18611
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: 0 <= dma___0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9919a561-8876-40fe-b781-a918591f680d
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8a6a3b2-9816-4f1a-b2c0-795d2e6f8f6b
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: irq___0 <= 11
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7965726-29e3-489a-890f-538be6049144
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: irq___0 <= 127
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6cb9b1e-ea47-4ed5-93bf-51c2a802a1cd
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: dma___0 <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34dfd7b2-cb5d-46e7-bd88-d60ac53a7999
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  location_invariant:
    string: i <= 2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a6314a1-6091-484f-a36f-f50a991df5fb
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6826
    column: 2
    function: w83977af_pio_write
  location_invariant:
    string: 0 <= actual
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4333c627-72dc-4231-9a3d-f6d3640aad31
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6826
    column: 2
    function: w83977af_pio_write
  location_invariant:
    string: fifo_size <= 32
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fa3f711-0fda-4764-a8e5-2b9a1ba1e393
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6257
    column: 6
    function: w83977af_init
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91ad2c5e-efc9-4f7c-b9fc-2dd5e165e4c3
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6285
    column: 6
    function: w83977af_cleanup
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d599caf7-5850-4dfc-ab46-69d8568696f9
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: 0 <= irq___0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1636768c-e186-45a7-80b7-51555cb89dd6
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: 0 <= dma___0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0eb31e7b-eb8a-4886-b0e2-3a68c81471a6
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dfa2eb00-ccdc-422a-8532-567d6b655fd0
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: irq___0 <= 11
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 69c821b9-ccda-4aaf-a11e-2d01cc301d60
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: irq___0 <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d5f67a2-9774-403a-93af-1b43a53083af
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: dma___0 <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ba39c8e-6528-44f0-9be1-26000ca443f0
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6531
    column: 6
    function: w83977af_probe
  loop_invariant:
    string: i <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ac5c18d3-9607-4dea-a950-7cba506f3958
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6826
    column: 2
    function: w83977af_pio_write
  loop_invariant:
    string: 0 <= actual
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: df09cb3c-25fb-40b7-b328-8160474512fa
    creation_time: 2023-02-02T14:23:28Z
    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--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 6826
    column: 2
    function: w83977af_pio_write
  loop_invariant:
    string: fifo_size <= 32
    type: assertion
    format: C
