- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b1abe00-9776-4215-8746-0c889b9836f4
    creation_time: 2023-02-02T14:22:35Z
    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--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: 2731e5fb-9fb3-4953-ae9b-8fbf04a024f5
    creation_time: 2023-02-02T14:22:35Z
    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--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: fb05d36a-db16-411c-aa0e-21e46c5b9d17
    creation_time: 2023-02-02T14:22:35Z
    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--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: a36214df-806f-48e9-b43b-d609de3c50c8
    creation_time: 2023-02-02T14:22:35Z
    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--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: 9d39b5d2-bf09-467c-bb1a-07859fe9f900
    creation_time: 2023-02-02T14:22:35Z
    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--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: fa1f9320-70e0-4af6-b627-a6c386873fb0
    creation_time: 2023-02-02T14:22:35Z
    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--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: 9f62914f-1240-43ed-9816-19b58a0456bf
    creation_time: 2023-02-02T14:22:35Z
    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--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: 9731b32d-12e3-4631-9683-3c04ad62371a
    creation_time: 2023-02-02T14:22:35Z
    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--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: 3bc63e6a-dd3a-4098-a0c1-066b37c8e970
    creation_time: 2023-02-02T14:22:35Z
    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--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: 4922ebf9-00d2-4f38-8ed0-70808d2a04ef
    creation_time: 2023-02-02T14:22:35Z
    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--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: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe1ee4b6-0f59-4a19-805f-7908e4c10db0
    creation_time: 2023-02-02T14:22:35Z
    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--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: 941bfafb-b609-4d36-81b6-ec7bc33eed7a
    creation_time: 2023-02-02T14:22:35Z
    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--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: 68e1bd96-0245-4b93-a1ad-cf981bb9e97f
    creation_time: 2023-02-02T14:22:35Z
    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--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: 50c51af9-0cca-4536-9120-042bf0979ec4
    creation_time: 2023-02-02T14:22:35Z
    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--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: f57c3b06-47ae-4c5d-b519-11aa9f43c3ff
    creation_time: 2023-02-02T14:22:35Z
    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--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: 6caa1422-e2f4-465a-ba1b-d9d26f5a6f8e
    creation_time: 2023-02-02T14:22:35Z
    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--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: f30e0b3b-8fc4-41a3-a037-ffe7e5003194
    creation_time: 2023-02-02T14:22:35Z
    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--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: 941211ea-2d3a-40dc-85cd-22ed40f1d782
    creation_time: 2023-02-02T14:22:35Z
    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--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: 8aac47a6-f3a0-40d0-a185-81995a32d435
    creation_time: 2023-02-02T14:22:35Z
    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--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: 1a46d4ba-a255-4981-85ce-d0ad57cc1761
    creation_time: 2023-02-02T14:22:35Z
    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--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
