- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9091759e-cf01-4340-bc72-cb8556c410a2
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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: 7bb98067-5c2a-4638-ad24-a76ed663aaf6
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 49
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: be8fc4e9-0fa2-4d79-a0f5-3658827f02c0
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 100
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9fa209ad-0336-4a23-8864-64f6f82a8acf
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 99
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0c44b0b5-ff01-41ec-b85a-118fd2cc3341
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 45
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fd41e78b-aa77-49a7-9906-e1d5f8caed45
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 67
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf7b76eb-53be-4af8-a6ad-964b7b6977f2
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 80
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 900d6608-01ff-41af-91e5-427b22170483
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 62
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 45d2e7ef-9950-494a-80c7-43d6e9862039
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 43
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 303bdfe3-cc43-4c6c-bff2-fddd36ff70f9
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 90
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3bf93e89-0600-4e7a-95cc-46c20abc2e3d
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 64
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ce19005d-e6db-41f4-ae15-6178ba7398c3
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 88
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a9e4713-81bb-4602-8779-d98a2c193f75
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 104
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03613519-458f-42fd-8e88-f4ab350c15f1
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 65
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fdf377ad-d5a4-4eb5-b4c5-6ff867f69bc8
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 102
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 853b6fe1-bfab-4c38-9bd3-e415be46d102
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 84
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5504e139-3168-4f87-9034-839b1bae95b6
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 46
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0165b0ac-a21f-4441-ae99-8b414ba42f7c
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 48
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: adaab04f-6fb3-49cd-94b0-3487199131b2
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 97
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e0bf6f39-60d3-4c86-bf85-956534f74de1
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 81
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cd6c792c-29a3-4a87-a639-d0cb2bb9f126
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 78
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 526da812-6b88-4672-9531-4dc28341dc13
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 83
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 80413d44-3390-416e-9b7c-2369be533ba5
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 51
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6125e9a5-c360-4419-a7b1-93b76a1563ec
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 86
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2cf65b94-cd4d-46b4-a961-6bc6ff575435
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 69
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2a0eb9d3-4e18-49c1-9296-bf4b2606f803
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 71
    column: 3
    function: thread2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 0584d530-22b4-4676-a7dd-7b774e10a5bf
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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: f012a945-ca04-4b10-84de-72ca7cdb6265
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 117
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 27aa74d3-d5e5-4cd2-88b8-5055706292e0
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 106
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bd25204a-9b09-4c49-80bb-f7da39e2ffc0
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 53
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 209673c5-b7fc-4d2d-bf02-7af891ec1ff8
    creation_time: 2024-04-29T11:08:11Z
    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/spaghetti.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/spaghetti.wvr.c: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
      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/spaghetti.wvr.c
    file_hash: 8451430e4d69b133c41912667dded61d19a596175a4065b8a2219f0d75763fd8
    line: 55
    column: 3
    function: thread1
