- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad7ecefe-dc73-4127-8924-e4e3e55ca15b
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 96
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2a25d06-79c6-4493-82d4-46bde922733a
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 97
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96b49012-7996-4cfd-b552-f1d04e436d82
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 98
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 069dc96a-87a5-4d19-b487-57d1ffa2cd15
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 99
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f048eb33-0648-44b1-98c0-cf4b0147da8e
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 96
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 576d8983-1d7c-4bfd-9a7a-ace1a7dc67b2
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 97
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b16c3094-9dcf-464b-9462-8e7a6754363e
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 98
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89294cb9-f19d-4169-a52b-aa5e35c29b73
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 99
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c8128c7-2027-469a-a873-23ba6ab448a8
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 96
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87e93cc3-bf83-4fca-a45a-520a5a5224a9
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 97
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfec70c5-620a-4a85-a49a-ab7f2221b667
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 98
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 850d4c45-4afd-4ca6-a541-60e060098803
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 99
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j2'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c55e5b5-e5f6-4c26-a972-16f54bb1e6a1
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 96
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4f2fa8d-a2e2-46a0-8744-8f487aedd1b7
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 97
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9101eb8-08ce-4aca-aaa7-7e6973c68180
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 98
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34f169c0-ef84-4480-9880-530e5c99dbe8
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 99
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j1'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76168c6d-0aed-4eb5-b4dd-b6804288fbd4
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 96
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= i1 && 0 <= i2) && 0 <= j1) && 0 <= j2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73d4b60c-ab1b-4b86-81ac-8b19a9b41e9f
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 97
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= i1 && 0 <= i2) && 0 <= j1) && 0 <= j2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 142dda0d-4783-4630-8211-a16fa7d893bf
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 98
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= i1 && 0 <= i2) && 0 <= j1) && 0 <= j2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38230bb0-1322-481b-9f16-065caf439d22
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 99
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= i1 && 0 <= i2) && 0 <= j1) && 0 <= j2)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 70a16f85-d0a1-4b90-af63-20d001d1a31c
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 576d13fc-5374-4e57-a98a-30eda274c0c3
    creation_time: 2024-06-19T11:55:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-proofs-counter-add-4-semi-Q67.wvr.c
    file_hash: 34bb015d05a3d6b765805bee36bd4c1bc3f74929c05e61a51973bc9a4fc2cfc0
    line: 95
    column: 3
    function: main
