- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ba7f747-2ffe-4b1a-9285-299c14d62c91
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 177
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == (_Bool)0 || b == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79f01cbd-91a5-4720-8269-e6c8277a3573
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 178
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == (_Bool)0 || b == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1283c938-cf1e-47c5-b07b-13b2ad53e088
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 179
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == (_Bool)0 || b == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ab9bd9d-5b56-4487-a6a4-25565a058c8e
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 180
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == (_Bool)0 || b == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ece4c14-49b1-49d8-9bff-c14a6c76cb5e
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 181
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == (_Bool)0 || b == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebcfd634-342b-40bd-9176-4a0b6a708fde
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 182
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == (_Bool)0 || b == (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: d10b7687-b0f9-41d2-8da5-2319e906cb53
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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: 60fc0ba0-1ee5-40af-939f-b990e4bb7b8f
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 83
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dcc36117-96b6-4a4f-8251-dc71a3d4d903
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 102
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 22062835-ffd4-4447-92b9-54548b203cfb
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 94
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d4d6ce8b-cb2a-487d-809a-f85a4d0d7f6d
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 109
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b8b314f4-0c13-49ec-b695-789cbd523202
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 151
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c15077a9-b621-4f09-a1a5-f864a25b22df
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 50
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bfff10b6-8824-45e5-863b-3bdeb045ab32
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 91
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f08b22a9-98c1-44a9-9182-7626d9058b02
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 90
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cdf0935f-ee92-4053-94d0-01ae7296bafe
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 55
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1a52ad7-fedc-4b19-8ddf-9f910651c255
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 105
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2aa29239-a778-4544-adf4-b857624ad2fa
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 67
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 71d2f97e-de8a-428e-862b-689ece9dc8cf
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 96
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 009ddad6-8486-4f1b-804f-8516d9eff6d4
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 69
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7804823a-7591-4ad5-ab7b-230bdbd0423d
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 112
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 077c32a1-95bd-41b4-bc66-7a21b64a4a3a
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 148
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 89a3a132-dbbd-4fa9-adf9-5a0b5d8017d5
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 126
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ee631a8d-c3d0-4572-8bed-88ccf22913a1
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 143
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dc7305bd-ba4b-45d0-bf94-bcbb9faf7873
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 93
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8170d29f-224d-46fc-829b-17944735986d
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 110
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a347e98-a578-47d3-9c52-2158d8164f68
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 53
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5730f00c-71ea-449b-bed8-04719a0c882e
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 145
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ec515677-f9aa-491e-8996-b127bfbb6290
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 86
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1470f451-fe24-40e8-8312-3fc3b00f0293
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 128
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8f6f19ea-2abd-4563-82bd-5472cfad2f75
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 132
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 67a5b45e-3e34-4d1a-b5fe-a681e4e69d1f
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 47
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8f0c857d-1557-4c29-882f-465a3650ee48
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 131
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: beadb721-225a-4343-9e1f-e5c6663f709b
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 113
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7fe8a38e-424c-4625-b618-9b7ef5ccf7d3
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 124
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef3b7a5c-e411-45b3-9f4f-768cff1630cd
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 49
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 349ee73f-e7a8-4bb7-bd70-b2275b42c57d
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 42
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03910aac-5f06-4fa8-a432-054fca184f55
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 64
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8308ef21-8991-42ac-b594-a36c24a299fe
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 75
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ee10af94-3687-4ef5-9eb6-4b837ec66d27
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 150
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 00bd1efa-5345-49c7-a0e9-a77cd3cda70f
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 88
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3ba22eb7-f65c-40b0-a393-fd6e14e3366e
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 56
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2b5c2b4a-1650-430f-94cd-cd216bd5ccab
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 52
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: be68642f-6275-4532-ba46-c60baa9953bd
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 77
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a0871d6-7c48-4348-9104-b00005a9a12f
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 45
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5d554296-dfc7-45e3-9633-8ce858e156f3
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 153
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7d72c29d-2d26-4c21-a357-42d7375ea237
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 74
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 128d9360-6a35-4816-b7c8-14116d453df4
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 121
    column: 3
    function: thread5
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: cb8be966-95e3-4763-99a0-462a84e59b75
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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: 9d480e44-1be6-4bcd-ac95-69c41be1083a
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 176
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf0ff2f8-8ce8-4e2b-ba87-8b6a70b11b28
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 147
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a406e76e-600c-455c-9683-45f491a745fd
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 134
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5fde7c1b-5595-44f2-8dca-31721fd98213
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 129
    column: 3
    function: thread5
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95a61790-1e95-47fe-af3a-0c27f5d3dcf7
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 140
    column: 3
    function: thread6
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6529f019-9cca-4edd-ae00-539b072b8107
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 107
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7cd35d60-a9f6-4d9e-a0a7-e2cc24176366
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 72
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 69d134f4-82cb-4e98-9d31-e838eed8dd92
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 58
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eff0aab2-94a1-426a-8d65-3a3bfa7afc7e
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 115
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c3df081a-5d72-43a3-9ccb-b208328e3bb6
    creation_time: 2024-04-25T07:42:51Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.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-6.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/parallel-ticket-6.wvr.c: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
      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-6.wvr.c
    file_hash: 0cfb19cf4d2e91498cc6b9015bdada7a33dfe09887340d8a9d79513b784b8b5a
    line: 71
    column: 3
    function: thread2
