- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f7d79bc9-4daa-4641-aae5-84b34e04eaec
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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: 8a4e2c52-c040-4388-ae94-d00c1e1b523a
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 83
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 578ac7e9-e476-4ab6-b7be-bb6298a87043
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 102
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9b04a9d0-eeef-451e-944b-89e7936556a2
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 94
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca30f257-38de-4108-850c-bd830f1240f6
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 109
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dba6e2a0-61c3-4e33-913b-2ff7848aaaf4
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 50
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8003a66d-5253-4324-b0d4-74c6998de080
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 91
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b343c1ca-6713-4f9f-a148-a54854e6dd5a
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 90
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c2198142-4b38-4079-8da6-8618e9ca7eb0
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 55
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b3880ad9-517a-4164-bee0-4b7eefa8d44b
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 105
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 06c9ab3d-0201-4b3c-a001-ed80eac75cfb
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 67
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 49bf151b-8df3-4ee1-b175-780f16143766
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 96
    column: 3
    function: thread3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 0db43ab3-4b09-4eff-bb9c-121b5889713f
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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: d802939c-549b-46c8-9334-1f5b8c5f0645
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 136
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: de22a76b-2102-4e96-b17f-fc3b336fd1cf
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 69
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: de1f450f-88b3-4d7a-ad4b-ef57341e0e28
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 112
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 15f15a0d-2c0a-467c-8c2c-e94b27d6b42e
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 93
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b4f3637-0598-48fb-a7b4-87ca8182c659
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 110
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 97665592-6b4e-47f1-9824-c690a378c873
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 53
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 83334793-0a42-4ede-8f9d-26bb581d8c74
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 86
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c43c2fff-9b9f-4016-878e-0fa431d84f34
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 47
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c1d16558-6c0a-4fba-9397-a361b1817147
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 113
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4df5137-c507-4f16-ad25-162efa0a5880
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 49
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 35bb5909-df60-47f4-8e5e-81e42c9b9014
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 42
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b4f13a0a-1591-4dee-91a6-de415058ee82
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 64
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4380e14-0f75-4e76-8dd6-c4dd72594f26
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 75
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3c21854c-d252-47b9-a0cc-81315681dcf3
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 88
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e4cfa585-48e6-48d0-9984-a5b808898f37
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 56
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1d9a9761-8f26-4a5b-82f3-1f6069047d1a
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 52
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3662cf55-0617-4a6a-bb0e-12f95d1b3ec1
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 77
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bb53e156-3fe8-4d2a-9c3d-b8314dd737df
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 45
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e5057eaf-f948-4305-8474-4e3b09a3bb30
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 74
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 00114585-69cc-4d1b-9e83-4cf0fb52a936
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 107
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 02d3f7d1-9330-40d1-82d3-40ed2b95f995
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 72
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cbf6740d-a21c-4039-beb8-7bbd8511cb33
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 58
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 19eb676c-0cea-4ac3-9217-a83e50da546c
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 115
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dc7468bc-4471-4560-98aa-440ddbf22841
    creation_time: 2024-04-29T11:07:13Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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-ticket-4.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-4.wvr.c: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
      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-ticket-4.wvr.c
    file_hash: d87195cdf1d0fd4bcadf67f37be6f46388ea22a2ec77b383d012327e126a2173
    line: 71
    column: 3
    function: thread2
