- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 903c6694-625d-4d74-9f1e-9858b1ee55ae
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: -128 <= ret
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2227aa5c-a5e5-4310-8c63-3af7456b04a5
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: -19 <= ret
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 605ff4f0-0f50-4733-8bb5-8a01b7362048
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: 0 <= cfg
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c35e5ae-fa0f-4418-8c4a-eae5aba3be00
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04fa7570-e280-4de5-8271-7df5b276dc77
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: ret <= 127
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c861ea5-ddb2-43e2-a582-59a1075af9c0
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: -128 <= ret
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e303f6a-6805-4d24-a011-206fca181dbd
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: -19 <= ret
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e5e1cda-47cc-4693-8152-7c5d4408f5a3
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27d2cf6b-4260-47fa-b8da-e9a702350c7c
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  location_invariant:
    string: ret <= 127
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41564db0-c3a9-4d08-8077-36474b1b9788
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6960
    column: 6
    function: nsc_ircc_cleanup
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39581d28-a210-47f8-99d6-74e7d5141eac
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 7029
    column: 6
    function: nsc_ircc_open
  location_invariant:
    string: 0 <= chip_index
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74b4da26-e97b-4820-a3fc-4a223448e8b5
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 8826
    column: 2
    function: nsc_ircc_pio_write
  location_invariant:
    string: 0 <= actual
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2de8dc7b-d524-4880-a9cb-3f1d578b7b6f
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: -128 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c1c6189-6e6c-4e10-92fd-569a09b3868c
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: -19 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fad805cb-ccdf-4589-848c-4ae1868d4803
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: 0 <= cfg
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a7607a7-38ce-4794-b035-27fb29ad07c3
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 180f65dd-35d0-4718-bc25-6aa4deced596
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6924
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: ret <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 52dc15d8-1ce0-465a-98fa-9b90c66337f1
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: -128 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d143306-30a9-420e-9928-a1cf0f4807fb
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: -19 <= ret
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa41760c-5fc1-476f-8749-56cfff8ba085
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2e282a0-9caf-4fd3-a643-16dbd765680f
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6930
    column: 6
    function: nsc_ircc_init
  loop_invariant:
    string: ret <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b5bef4d-1818-419b-a10f-438d0b3c00d6
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 6960
    column: 6
    function: nsc_ircc_cleanup
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77776a52-f8e0-430e-9b32-1b4159b28c94
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 7029
    column: 6
    function: nsc_ircc_open
  loop_invariant:
    string: 0 <= chip_index
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f57e24c9-b13a-436c-90e8-1f5d51270c36
    creation_time: 2023-02-02T14:22:39Z
    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--nsc-ircc.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i
    file_hash: 4936125952f00e8b7bd10cd011fdd99ca1fa98c1dbf62cbf7f8d6248efd38f07
    line: 8826
    column: 2
    function: nsc_ircc_pio_write
  loop_invariant:
    string: 0 <= actual
    type: assertion
    format: C
