- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e72a26f-094f-490d-9cde-d40cc6896d47
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 0ccef273-e515-4e67-a508-4877be360c56
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 5cae8860-e92e-49ac-8a9d-1a499c7f97a5
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 6c7e3370-6f83-460a-99c0-54839025d076
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: a765e7d4-d241-47b4-b08e-cf80b03a3f7f
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 4d66bbd9-2e7f-4fa2-a951-8a40d559d163
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 0be69236-4585-4f5c-9ab2-a0b6af093565
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 91ce6cb4-49af-42ec-a5b4-ce80576952f4
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 55467dee-8f45-4c66-9544-5a312a81e90d
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 0ec24f80-c980-4ccd-99e2-b7d03b186bb7
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: 4099ac7f-9715-4960-a0da-de2904636c71
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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: daf16eb0-6f0a-4adc-8c0c-54b71714af1c
    creation_time: 2023-02-02T15:13:52Z
    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''
        ''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
