- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5daa11a-f31b-4b51-8805-a8a4275b0008
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 180ea29d-9c49-4130-88a5-271b3adca41b
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 91c80242-9bba-4520-b335-021778ded6cb
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 8b234514-7be8-402c-aed2-7ce6c19b9bcd
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 8bc8f88b-d899-4477-b3dd-538c7e2fca96
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: cffbcae9-745c-420d-b940-64182df3c360
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 3288f29d-8ead-4b38-b6d2-b299f8582c42
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 1d412411-d5c3-4175-a43d-5d783d2f650f
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 7cc011b4-0890-4bc6-8554-41ce9b359c31
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 87982557-caae-441d-b103-2056a41000ff
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: 654f5926-f319-4494-bb8c-6a581b9dc7e7
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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: c2718ce6-eee6-463e-8b7a-04c067bf2c35
    creation_time: 2023-01-31T08:58:53Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-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''
        ''write+lock'' ''--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
