- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c74dffc3-80a2-4ed1-a102-34484872237e
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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: ee408f71-3167-4fd4-8f36-c56a26f70f52
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 83
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95710944-a430-4b6b-ad33-9f9bb274837b
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 102
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7e9e5262-9ddf-4cb1-824b-48ac6955cc8d
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 94
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 13e61f06-ee08-4727-bd50-08f9e73b2e02
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 109
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 71697f88-d857-4ee4-aa6c-c49f1768c6cf
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 186
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb751052-1ff5-4e23-8ea0-13f893bacce7
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 151
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f45db7a-c18c-4676-9056-f98cf8793748
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 50
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f556de06-b5b1-4ba1-a1e5-8cbdf246bb3f
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 91
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 63b7c769-1391-402c-8523-a546c4247bac
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 183
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1b1996a-bd7c-451c-9524-f39c9c23e93f
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 105
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3ffa848e-fcd9-4a9f-86d7-e48add7abca1
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 188
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d54d85b-f17e-4ee4-93e7-d65c4d4c7a3a
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 67
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 34a0aec7-9129-4b19-aa69-bd5239ce795e
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 112
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 49538d35-d070-40b5-bded-1ded636d4763
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 148
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e2414a46-111e-4b5e-b07b-3e54a458db79
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 126
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 41b69790-ec8e-44a6-adde-7d482c663f1e
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 164
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 83b8abd7-e004-4450-aa46-70e4721c27d8
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 110
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c238f1a-d147-41a5-8c24-5d14fe77faa8
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 53
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 87593ce8-1c14-4aac-a71e-fc3e1e19332f
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 145
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6c3ae073-81c6-4794-a891-21b4809477a4
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 172
    column: 3
    function: thread7
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 151a9102-c90c-4ead-bfc5-433c554ade77
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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: 50617c53-d241-4277-a084-3882d4bfa7c0
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 216
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e26620f8-ec86-4f3f-905b-753e2ee49aff
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 169
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a72aedcc-84e5-4a68-8e32-b8ad8f8a9ef5
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 47
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f191fc85-df9e-468c-84ea-b11a71f7bde2
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 131
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 727cfecb-8fb2-4304-a66e-ef83fd432fa1
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 159
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9894a6ac-f3f9-427e-9a4a-299287026d07
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 49
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d5d2d78-98ac-4081-a73c-3f032f88fd7b
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 162
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 555b92db-ce69-4302-82ff-b40b6274fd77
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 56
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4060ffae-7f7f-4754-ade1-631f0ee5b685
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 52
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: af9e7fa8-d9fe-4fc0-84bd-589bb7f8a6a2
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 77
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: beb47f6b-c48c-47c0-b7b2-f6feee4b89fa
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 167
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6b3c4349-fa45-4c1d-baef-908ba38d8592
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 189
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4eec7e4-a586-4022-a1b1-454511e95a32
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 153
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 85c04284-73b8-4d04-bc60-3f77260e60d4
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 178
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5814e0f1-7276-4506-b77f-3ea7cf997b48
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 147
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eb54262a-c859-4c37-a31b-7d1786d0e605
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 134
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7959e4f1-7f0c-4ebc-bc7c-1a1983f47ba1
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 181
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ea8bc722-46ef-4ef1-83e5-e8a632bf102c
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 140
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5c54e025-1c1e-40ad-b4a0-a0aef2e70ed3
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 191
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d72c48a9-e563-44a8-b720-3af19361d92b
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 58
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0edb8fb0-4866-48b0-9835-577b10541589
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 71
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fa4335aa-16e6-4932-9d96-0c106833acc4
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 90
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c9accb0a-82fc-4edf-a860-74eb64f5a43d
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 166
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: efc36f43-b27a-4bc8-9cb6-4a7236a85f6d
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 55
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4acd4b80-9e92-4710-b139-2bb83609f003
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 96
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6f7f38e-3080-403c-a956-efb0ab1ec1f1
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 69
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d1f7344c-c307-40bc-96a4-e2daaaff4b3d
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 143
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0f302e3-13f7-4fb6-9575-0a98de64a278
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 93
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 12893998-f34e-4841-999a-1d345da19022
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 86
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d6ddffd-94ab-4d37-ac63-40cc8932f771
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 170
    column: 3
    function: thread7
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2c9b1be7-0500-4c09-aa7b-dce0e0e3e6af
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 128
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 98c1837d-8983-444a-bd25-017f140f3fed
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 132
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: be98ef71-61cc-476f-89c8-2e426bac8933
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 113
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: abbcb9a5-0e22-44fd-9978-710b47b7dd89
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 124
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac7398a1-8c1b-4aa4-ae40-18698d5bfcfb
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 64
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f9af50ab-e89b-4586-9d8e-e48932bb3177
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 42
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1853a301-9ec6-4a5a-b2d8-17a79701ed04
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 75
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c35bbba6-ec36-434c-91fc-95a8a2acd132
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 150
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac396a7d-cee8-4f62-b7ae-522b9a615215
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 88
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76f42bec-b677-478f-ac19-f11affaef2d8
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 45
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9d6e6a1b-0b97-44a7-b5c8-15b3f5429176
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 74
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b4fb5044-a5d6-4a20-9968-5d0055edb855
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 121
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c87bb3f5-b6a3-4112-8f40-4d9ea92afc12
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 185
    column: 3
    function: thread8
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b620f3d6-2a90-49dd-8182-a1e90fa1b422
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 129
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4df2f703-d9d2-4dd7-ba89-b4f748895f85
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 107
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3d5e36fa-539d-4b1e-82ba-33b0567ea835
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 72
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 372c98fd-9d63-4d8c-af75-9a5c2d6787ce
    creation_time: 2024-04-30T09:43:00Z
    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-8.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-8.wvr.c: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
      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-8.wvr.c
    file_hash: e9184a10f76289bc351ce16b4243b6d0e46782fe8318237a8a819d2b43a92673
    line: 115
    column: 3
    function: thread4
