- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13da98ce-07ae-418c-bb39-a84301c3b639
    creation_time: 2024-07-04T12:05:11Z
    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-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: 24c89cc3-04af-4bf4-8447-15ee91d85a11
    creation_time: 2024-07-04T12:05:11Z
    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-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: d19fab08-04f2-4583-a27d-a0343cfea651
    creation_time: 2024-07-04T12:05:11Z
    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-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: 3f8c4cb7-0d74-4f6b-93cb-1ff0636b9075
    creation_time: 2024-07-04T12:05:11Z
    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-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: 5bea15ac-4272-443f-9a60-3018bf12a3cc
    creation_time: 2024-07-04T12:05:11Z
    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-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) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: 02652572-6a15-4521-9d63-b60a5f679ac9
    creation_time: 2024-07-04T12:05:11Z
    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-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) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: cc112a7a-2776-4f43-88a3-0a5a1ccb53ad
    creation_time: 2024-07-04T12:05:11Z
    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-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) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: 4f2cf874-396f-48ef-90a4-cff67ed83bfc
    creation_time: 2024-07-04T12:05:11Z
    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-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) && (node1_state
      == 0 || node1_state == 1)) && (node2_state == 0 || node2_state == 1)) && (((((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: 9fd104fc-312d-47fb-a0cc-4f67566e616f
    creation_time: 2024-07-04T12:05:11Z
    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-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: de3a24eb-a8b8-49ef-b06f-c3a9c1b4ccbf
    creation_time: 2024-07-04T12:05:11Z
    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-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: 13d2db50-293f-4b42-95d7-f4f12dd49261
    creation_time: 2024-07-04T12:05:11Z
    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-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: baa6c1c8-6cd3-4803-80a4-bd776479bd98
    creation_time: 2024-07-04T12:05:11Z
    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-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: d691caa2-16d9-4f70-936f-8b3735e3b82d
    creation_time: 2024-07-04T12:05:11Z
    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-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: 1a4deb69-30ea-4c06-bbb7-0f15e1cda4d0
    creation_time: 2024-07-04T12:05:11Z
    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-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: 5d88de3f-df78-4d5e-aafd-4cdb30bbedcb
    creation_time: 2024-07-04T12:05:11Z
    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-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: a9591e94-7d96-481d-b309-e9fa2ed64f8e
    creation_time: 2024-07-04T12:05:11Z
    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-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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e524eb83-3cf1-4f7f-888c-f54a365c87f7
    creation_time: 2024-07-04T12:05:11Z
    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-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: 70738037-ce37-440f-9010-de4cc088ce11
    creation_time: 2024-07-04T12:05:11Z
    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-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: 01c5114e-cb39-4289-a0bb-a869ee636931
    creation_time: 2024-07-04T12:05:11Z
    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-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: 40ffac11-7f18-4d54-9dfd-39700d7e8f50
    creation_time: 2024-07-04T12:05:11Z
    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-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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 800b7d44-3197-4836-8e4f-3c1bbf01aaf0
    creation_time: 2024-07-04T12:05:11Z
    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-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: fb9d16ee-825d-48dc-8e54-8b0137bd7a90
    creation_time: 2024-07-04T12:05:11Z
    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-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
