- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c4c1253-cd41-4049-bb7f-56ea0d04ab89
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 141
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (v_assert == (_Bool)0 || v_assert == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfa5dc94-2dbe-4237-83fc-a08e4ab70486
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 142
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (v_assert == (_Bool)0 || v_assert == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a47ab556-50a8-4e59-9d63-c8b4e260944b
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 143
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (v_assert == (_Bool)0 || v_assert == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25d7e4cc-4b89-49a5-be30-c4456ef42116
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 144
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (v_assert == (_Bool)0 || v_assert == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 227506c2-1b64-4225-8c0a-ce3d388fdbff
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 141
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (v_assert == (_Bool)0
      || v_assert == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e4b0040-1a8c-49f5-8ddd-ed58f1dae258
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 142
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (v_assert == (_Bool)0
      || v_assert == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7a97ca2-ae0f-4602-8aa1-e1343894e68c
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 143
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (v_assert == (_Bool)0
      || v_assert == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0354bbd7-6e9a-4127-addf-08856da229e4
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 144
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (v_assert == (_Bool)0
      || v_assert == (_Bool)1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7b5c5598-917a-49bf-8b54-068e031af032
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 06c8bd44-8d05-4f54-b2ea-e8c9088c000f
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 55
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1d4c39f1-1842-4594-8499-e2d8ebf1017b
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 81
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 87079d44-a463-4a2e-9fd2-62e2c16917b9
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 105
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1cbf3ac6-fa48-40f8-90b9-23bcd176d378
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 67
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bc1ad51b-9917-41fe-a5f8-69cad57ccef4
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 51
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3b08f218-10b3-4419-92eb-d72021afee37
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 98
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3a8bb5f2-c2b3-4c79-b95b-56ffbb6490ef
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 84
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ab2c05f6-1096-42fb-b455-44d4e368cc03
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 75
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ba42cfe4-4e02-451f-b24d-b914be4c5d75
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 71
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 835202e2-d3bb-4081-bb55-7b902621218e
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 102
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ce2ad326-b62f-4da1-b18e-228ac566818f
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 59
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 620aa37a-b75a-4ee7-92b3-95930abb40fa
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 86
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09e4e6b6-779f-4ab7-8bcd-b74a271a3e32
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 108
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a3aebf2e-4461-4778-8a22-fa0ca4bfdc32
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 49
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 52ea6f9a-71cd-47a9-8d6c-ceafa05f402b
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 106
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1484040-1c3f-4406-b6b9-45cc4a2917a9
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 76
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3f25df6f-1e88-4d3f-a24c-6db51f4af3e8
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 103
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6b10b862-be24-48f4-87a5-9b3aadef1aea
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 117
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c4b59e39-05bb-4b75-b35f-259ae332ba72
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 69
    column: 3
    function: thread2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b81b57eb-60f1-4247-90a4-33e885c6d488
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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: 0ae4ffb0-defe-458a-a715-5491a5ab5158
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      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-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 140
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a95de7b4-e847-4fef-8637-26c8f08d2353
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 83
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: df526650-eaf6-407f-8efa-b68a01ffa72c
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 94
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ace84cbb-c11b-48b2-a573-7c04dbd862b6
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 80
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0cc291b5-e508-4f15-801d-8475d8a95be6
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 115
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dd98185f-238f-4144-9ae6-dc6df456dfb3
    creation_time: 2024-04-26T10:52:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-prod-cons3.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-prod-cons3.wvr.c
    file_hash: 41874b69ed787f1d4b0fd199a95bb437bfc8aab0f734c194621d2ef33cc65cc9
    line: 96
    column: 3
    function: thread3
