- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b793a43-a4f3-4cbc-ba7e-5cb04714bdb1
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 8ef2c53d-18e9-466d-b57a-b030954c5b9d
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: a135f398-fd59-4fdd-98fa-1225efcfff4f
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: c9590b1b-bc4c-43ef-a077-555d5248b35b
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 8d159e74-cfea-4e76-a01d-d4ac2873fbcc
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 473d1075-1298-413b-b2de-88b71dd15d4a
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: a617cec1-4156-4c0d-8013-16367b26cced
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: b34c057b-e30d-4ad0-9503-23737502e480
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 421d3a7f-578a-4132-b6da-243451026541
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 612156f0-4bd9-42da-8f7a-0121cfb1c0f5
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 3a3e4e4c-c481-4678-b7c2-26d93c20469c
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    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: 3846088c-e103-4b16-bb91-f4e5259d5acf
    creation_time: 2023-02-02T15:13:20Z
    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-1.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--media--platform--marvell-ccic--cafe_ccic.ko.cil-1.i: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
      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-1.i
    file_hash: c58bc364903aab3e0f143ea0940d1f6b914be71bc821bca2b70310f31f2f21f8
    line: 9561
    column: 6
    function: mccic_irq
  loop_invariant:
    string: handled <= 1U
    type: assertion
    format: C
