- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ec3b9c27-6f8b-485e-bcbc-bef9d578011b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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: a1a27e1c-1fae-4420-87cc-a42c77aa700d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 148
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 02c31c0e-4401-4f3f-a42f-f5758d4ea53b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 161
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0efeecda-e345-4690-9489-21052166df5d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 200
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5dcdd089-9b1f-4f2c-b871-38353ef8a872
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 116
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9b71f387-9ddf-4e5f-8f58-7e27d7b8375b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 226
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe7d7431-6d78-421a-93a0-04775f9a223c
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 244
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 49629163-e3a3-41c2-8b34-3697eb17e888
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 128
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5218178f-0c22-40b6-b0f7-80bfa8f73719
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 173
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 16ac6cf5-f6e0-43de-a248-603458bc2925
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 215
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e3d29892-6484-4042-a4d7-67de1edb62e0
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 66
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f701f0a5-006e-48c8-b208-e472bc5b8465
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 109
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 07237e91-ba2d-4a03-883c-f2bc9bf29e1d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 225
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 44fb0b5b-245f-4416-b696-6c88587ab544
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 67
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cc3520fe-c196-466c-b172-e6eb250cf1de
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 179
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f2625739-bf2e-4f18-b33a-2729bffb4961
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 239
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 950692a2-ceb6-4c33-adce-a3c49e0df034
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 163
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2db9372f-fc15-4211-8c22-42cb43f9527f
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 100
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e27d58bd-4f7b-4445-9d90-1556a53867cb
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 57
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 59441c98-0df2-47b9-a499-e2af20e0bbc0
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 241
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9dc94b53-471e-4b73-9a0b-6c4bdaa9403a
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 103
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 63c620eb-69c8-4ee2-8713-071480d707f1
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 75
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 287b86cb-3d1b-4475-b11d-363e216ab8d8
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 82
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 886897d9-9537-4e90-a011-f75bb6b41bb0
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 47
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b368bb34-dba8-49f8-96eb-a4a0300d7db4
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 137
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 69bc60b7-8377-4ac2-bfa9-003a5386d287
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 171
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 70976eb4-298d-4014-9e9c-4ad39acb7bc2
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 201
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: db2606f5-93b1-4715-a0be-d4be0c8f4a82
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 187
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 655ba166-23b4-4448-a6ae-aa6659df7308
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 219
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42a2035e-c924-4c14-a77b-98754796aeef
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 115
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c4d1ef6e-06da-42f2-bf58-8a9ac1e043ee
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 54
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5c7e338d-1c37-43ca-b995-7340b3876943
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 157
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 712b417c-c48a-4d21-ac0f-e2a84c7bdbe3
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 182
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 93b570d4-44eb-4a57-9c03-e42a3fcdd79d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 59
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 715e4f5f-b624-4f4c-9bef-c382bee73c68
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 151
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5f16911f-7dac-4981-89d2-b6a085ac9fd2
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 165
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 78378c0e-6972-4dc9-9361-e78c537438ad
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 174
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a9f87284-78ae-4290-be8a-60e45c1cc1a9
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 113
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9a733e8a-d52e-40e1-9b8c-ec5aed71687e
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 206
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e252ce9d-99d1-44bb-93ca-1e3ad8c249ac
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 184
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 829f27e2-61c0-40c2-bf0d-a636a6320fba
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 61
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 21b50d95-900e-4690-b2ed-56455e0d97f6
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 111
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2e8b0927-b95f-42b8-9c91-8ad7df521292
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 135
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e71082a9-49da-4551-98da-ef8bef18caa5
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 138
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8e3ca79b-af8e-47ef-b3b0-c2d0444c84cd
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 198
    column: 3
    function: thread4
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9349b46a-4f05-43ed-90bb-6363342b3220
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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: f60fda99-5dbc-4bbf-a30e-b556482b0f5d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 270
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6e204ba3-2176-4f66-bdc6-436ad8cbf3a3
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 160
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6732b7b3-2dec-42bf-b00b-f7e024eb4949
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 73
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2fc5181b-9422-4091-bdba-cf32c126cca8
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 127
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 199a7925-b697-4249-adbf-5676301fe054
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 88
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2faa75ca-81bc-4b98-a3e9-4f3c40220a45
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 102
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3bf8d70e-cc0a-461c-a226-11cfbd159e2d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 186
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0c04a946-582b-4446-8b39-3b43bb441691
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 56
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3f2209d1-ac89-4801-bb63-4c648506ca06
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 158
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c66653a2-739c-4644-b1ad-eca5a718bb66
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 69
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e9058a90-0ef0-447f-a9c7-9f5d012bd584
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 48
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: af6ae261-d857-483b-93be-52708c073e7e
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 106
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 619bb757-f6d8-4b7a-bdb5-a4fd669a2bcd
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 94
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e9950321-140b-42e6-9324-2e875bffb712
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 168
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 59e31cf0-576b-482f-9649-76c39042a25e
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 213
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aac763d8-1af3-453f-8345-b5d027cc8875
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 190
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c83e5e20-9fc6-47c1-970b-dc487b8e9e34
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 105
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 235c5886-b912-4437-a56b-05ce77aaf990
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 203
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2600ea94-e705-4996-b0d3-69994fd63f2b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 229
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4936a1e6-263e-417d-8d0b-d6ed88b36cd8
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 155
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 78e0bfc8-cedc-4106-873d-f52f26b8280d
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 97
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b5b586f-7989-48f4-84ce-47778d0bc4de
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 53
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2d4ad2da-b5bd-4b38-9dcd-704204ed5684
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 223
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 835105c9-bb36-47c8-aaf6-058227725eae
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 152
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 726baf78-42fb-4dc4-9617-57f411892c5a
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 78
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5a8fc06e-1fc7-4190-9a7e-504904e6ba5b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 154
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9020385e-66cb-4b66-9adc-62b846fb7187
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 99
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 37e5fb0e-1611-467b-af35-7a8031b39289
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 134
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9026b2bd-6021-42df-b25f-c118bf8d41cc
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 180
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f65af1cc-60d1-4aa0-b74e-fb894c65d9c1
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 132
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 06640944-766c-4d26-80cc-4864b1ac8f23
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 85
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e7649dda-29e6-461f-9d6f-7788c673bf0c
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 130
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 831efcb2-e149-4ee4-9b6f-b259c4366d9b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 146
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6174b6f0-2e1b-4171-83d4-4da0866db4b1
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 121
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6ac36884-8569-4b0c-ad24-201ea53f99db
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 234
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 50b0848c-6ac8-444a-9380-f9f0901c3d94
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 118
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4c3212b-38a4-4476-be78-7df43615a59c
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 122
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b71b1529-d758-4869-b282-980665559462
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 86
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: baa9ba61-b9cb-4901-8dec-0e69505c993b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 70
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9b3d313c-3dff-48ae-ae5b-53fd806db565
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 228
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f37c4165-69a9-4c69-bf39-44d8cb2cc367
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 44
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4be4d20e-c7e7-4a90-848e-5bcc1e02f743
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 83
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1cfbf982-b1d7-41fa-8d25-54ec45762496
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 50
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d5bf5c3d-c62c-48fc-8726-f0116066b0b0
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 42
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94c365aa-1212-4eb4-97b8-628dea586803
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 64
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a658c957-97b5-4668-9449-9eb6b3e88d0b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 124
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c033687-24c0-4fde-ab8f-11607553de1a
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 108
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 43898967-0487-4561-9fb9-ce62e1f224e3
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 76
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac0f74f3-8f3c-46e4-b7b5-096846ba11a4
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 51
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 50767595-cf14-4859-8c75-32f5a9526bff
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 217
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 88df0ca6-c52c-4dfa-8fa0-fb06e1f8a86f
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 231
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e9d08656-fa99-40ae-8000-f44fa08a49ab
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 232
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a300bcf-4e67-448e-bf2a-4fefe4a6e107
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 119
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8a71c292-12e3-4a24-a628-247d83e6c99e
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 212
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 73b9b714-aa02-4c05-9f0c-b087d111533b
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 204
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d9c921c9-d7cb-4a03-9ae0-bbf06fe2d157
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 210
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 84646c51-071c-4930-988f-574b3e047e71
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 167
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 81612d72-a90c-421e-8613-902693190ebd
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 149
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 410f65b0-ac5d-46f6-8338-5b9d52039e98
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 45
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a061902e-307a-432e-9653-7f1952867bf8
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 238
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca8fef7d-d883-4fc4-890e-94032670bf19
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 63
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4702afa8-5d54-458c-9e30-951f7be3e034
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 170
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d950703e-db88-4a89-bffc-7b3c3f6d70c0
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 207
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c992c741-00f2-4fea-8879-291859c2e240
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 125
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 636b7b47-fcff-4750-afd4-67ea37b30f5c
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 80
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 73a3e8a9-6a2a-49f6-8c60-317d9a8fb066
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 189
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c6e132f4-d585-4cdb-b950-b03f8bb155fb
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 222
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f9a6ef15-3c1f-4297-8385-a865897fa6b0
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 209
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8b0725b3-77b6-4873-a497-74e579f35ff5
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 96
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a45b9f4c-1531-4d26-b252-9ffaf3711935
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 236
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6e6ebc42-d453-4bee-905f-42ff60d70237
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 72
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 13ecd316-3ac6-40ba-865a-1872ea2e74ac
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 177
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0bd7cb45-e214-4e66-9e79-c461499cf6cb
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 176
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3200a623-e00a-4322-a3fe-33f1c2d2cafc
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 242
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2fc3dcb3-3c90-467b-b2e6-90f0963c3c7e
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 192
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f9e0b7c-162c-4358-933d-f25d150bad9c
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 140
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9da0e4c3-17dd-46e2-83b2-8a68c2a3a88c
    creation_time: 2024-04-29T11:58:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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/parallel-bakery-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-bakery-4.wvr.c: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
      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/parallel-bakery-4.wvr.c
    file_hash: a42fdc99fbc54512a7829bd297e0f02fe251a511098f304812399f6e9de1d8b6
    line: 220
    column: 3
    function: thread4
