- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ca241a2-2ec0-4468-91bd-565af7d82357
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7402
    column: 6
    function: mcam_reset_buffers
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d364233-dd13-48b4-8736-90768fef66ee
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7543
    column: 6
    function: mcam_alloc_dma_bufs
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efb90395-6553-4750-8a00-74d2fc8c74b7
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7543
    column: 6
    function: mcam_alloc_dma_bufs
  location_invariant:
    string: i <= 3
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a975324a-bedd-4a73-8798-3030ecd9d725
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7602
    column: 6
    function: mcam_free_dma_bufs
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70f8e21b-4ba5-4b8b-9a89-9e252f377df7
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 9544
    column: 6
    function: mccic_irq
  location_invariant:
    string: handled <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76a03c0d-98b8-4022-80a5-96e9b7cabb7e
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 9561
    column: 6
    function: mccic_irq
  location_invariant:
    string: handled <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3013440f-7541-42ff-929d-45b58be46192
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7402
    column: 6
    function: mcam_reset_buffers
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e396c8c0-e660-459e-974d-b1c659a1f954
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7543
    column: 6
    function: mcam_alloc_dma_bufs
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dd96ced-a96b-4663-aa35-3fb83cdeef98
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7543
    column: 6
    function: mcam_alloc_dma_bufs
  loop_invariant:
    string: i <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c3a814eb-0f9f-496b-bf37-7909f0e5e78c
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 7602
    column: 6
    function: mcam_free_dma_bufs
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 07f00e3d-cbc4-4a05-b453-b9df6c915d2f
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 9544
    column: 6
    function: mccic_irq
  loop_invariant:
    string: handled <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4994c1e-cffc-466d-b255-0f659c6f140f
    creation_time: 2023-02-02T14:24:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''mine'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-2.i
    file_hash: c540d72ba5e6bf3b6f86e26d5c4995e6374096169e4f4b65620ea58c7f08d081
    line: 9561
    column: 6
    function: mccic_irq
  loop_invariant:
    string: handled <= 1U
    type: assertion
    format: C
