- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41b5c24c-5107-460e-a09e-a564dec1cfc4
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 622af9b9-0724-409d-8174-ac75556e02f4
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 9289bf7d-377c-4f43-be6b-5c56804dba7d
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: a938ecff-4854-4da7-8bb8-684b1a8f7fa1
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 86a8b958-2da3-4848-ad9a-52ae7b6def7a
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 3d404130-52f1-493a-987f-05716cb50b61
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 063b2b6a-4a94-4d4f-b83a-36ece08c1cbf
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 35c75cfc-e5e4-4010-8e15-523fd7c1e35d
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: d6d3eeb4-ab73-4832-a4e4-4e3e00ae6850
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 0bfbcf6c-7d7c-4c5d-9f5f-8feffb94b54d
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 2275718a-4e9c-4284-b94e-bd95fdb127f5
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 3030ff94-9148-4e4e-9af0-96b45dc74131
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 8a8baebf-424f-4d07-bfbf-40cc8fa4f8d4
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: a9483aa7-fed8-4158-8f51-4152959fe154
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 9f966dcf-1c43-4c56-9364-dc81fedda5a1
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: fcf8d34f-2873-4dca-b917-cf0fdbfccf76
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: e68d8b4e-c762-48c0-bacd-a102bb729c5e
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 2f307fa4-7a93-4de7-86cb-7e41d123cb1c
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: 6df8617e-7193-45d6-ab57-a1449602c5ed
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: b9a8e259-f4ad-4ec7-b6e2-279551efcce5
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: f24fa509-14ea-4c21-9b7c-d24b6071364c
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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: da16f797-4770-4de7-a776-3059158148d0
    creation_time: 2024-07-04T12:05:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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
