- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ab022c3-d4d9-4cd8-ac7f-274f728d64de
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: bb6366c8-4617-4e97-afac-1d249bdebb43
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: e4852699-5e12-4e50-9dfa-2bd6762bfdc4
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: adc8c371-f978-4814-aa27-0656fe8fc9d8
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: ae71f070-4ba3-4d6a-aecb-224a4633e4fe
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 15fe47e8-0d28-49e2-9485-d6d7cce1c26a
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 292cb195-f2a1-4166-a994-ef724c83289a
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 9f0bade4-a9a7-4183-80fa-e6802c84a2b3
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: c209ecd3-371e-4add-92fb-e8e0298acf02
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: e16642df-2f1f-4adb-892a-de1a99d2501f
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00057dd6-e3fe-426a-a981-ebaf378cfd59
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: fifo_size <= 32
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27af60f2-d221-49b6-958d-4f39f86351ab
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 7acec000-73c8-4015-909f-bf9f2fce1690
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 08209d25-6abf-4842-9ea4-d359711274f1
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 547c003f-0365-44d4-945e-2436fa78be02
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 8274af57-b2e5-4e5c-88fb-412671110e98
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 631da3fc-12a5-46be-b769-d5384ecd89a2
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 358688ac-a102-4664-b367-1124dad27592
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: dbb6a85e-7868-4883-a16d-afaacb435de3
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: f59908ce-57bb-4cf9-bb65-a82bce5d3574
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: 55583826-ac1f-411e-9e2e-43f2f7f67619
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c407b949-58ae-45d5-b833-d10a33ce0acb
    creation_time: 2023-02-02T15:11:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0
      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: fifo_size <= 32
    type: assertion
    format: C
