- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8891e507-5057-44b7-b7f4-42a044950c01
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43079086-3999-47df-b797-8cbb490047d2
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e56416b-1420-4bd3-864c-50c14bc030fb
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80a91be0-bafe-47ac-9194-81d7ba051ec7
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d41ec12f-7904-4cf3-a3fa-62d7ce95f98f
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f041276-f65e-4014-94ad-6eff2b72c4d2
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6624aff-ef9c-408e-b38d-f170f69d6678
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 777f35dc-3620-4eef-baf4-6ccdee9a4506
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((((manager_state == 0 || manager_state == 1) ||
      manager_state == 2) || manager_state == 3) || manager_state == 4) || manager_state
      == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1603ade6-c91f-4914-8536-784d8ae151fe
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node2_state == 0 || node2_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2764d4ab-fa41-4be3-9aa0-6907eae517df
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node2_state == 0 || node2_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d995f8cb-c1c2-4451-b7f6-6db7edab79b8
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node2_state == 0 || node2_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9621b364-5469-4122-b7eb-a1d0f1030d2d
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node2_state == 0 || node2_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fda5293-9ce3-46c3-9887-2948d7f1cdc8
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node1_state == 0 || node1_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8cec9dd-9355-44ac-a483-70c0402dfee9
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node1_state == 0 || node1_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6afa709-beab-418a-ba5e-a1f1f07d5151
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node1_state == 0 || node1_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 201d6e60-ddd8-4b8d-aef5-a4b36fffef79
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (node1_state == 0 || node1_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58e3774f-8c57-4fe9-896e-315022e096c0
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 197
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (client_state == 0 || client_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a1bed85-1150-4efb-b5e1-5a82e13f306a
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 198
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (client_state == 0 || client_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78ac69e2-1073-4785-a191-508f76c488dd
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 199
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (client_state == 0 || client_state == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfcb06ba-98e9-4ef3-99c9-cd0b0e521b3f
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 200
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (client_state == 0 || client_state == 1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1e4e9584-aae9-49f7-ac5e-15974887facf
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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: 17e77ef1-de30-41aa-b3d3-4645e3503028
    creation_time: 2024-07-04T11:42:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--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-bad-commit-2.wvr-bad.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-bad-commit-2.wvr-bad.c: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
      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-bad-commit-2.wvr-bad.c
    file_hash: 5bf746ef76f8c8352051d8eb5f02d7a475e14d238622e290fcb51135a3348206
    line: 196
    column: 3
    function: main
