- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a9112e9-0fbd-41c7-94c9-740518e8611f
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 139
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5c5bd1f-bbb0-4e1b-809c-283e91849101
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 140
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47ce799f-2c20-4abd-950d-0337017434dc
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 141
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eba387a7-65d4-4912-9c6a-1e0b0bdf65b9
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 142
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93d82e92-ca75-4d4c-a714-ddadd92c77a9
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 139
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12af77ca-3230-4df2-a302-75008542ce98
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 140
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4071b9e7-6932-4fdb-bc84-155cc397d8ad
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 141
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: deabb148-212f-45ec-9c23-3af21b608b8a
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 142
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= i'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6871c550-2ca5-4eaf-9998-6964bb5e7a98
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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: 71d2ef12-4c83-4f83-b969-343b60b1e278
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 58
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c93a8c03-bf34-4997-81fc-a4f61a5d71a4
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 57
    column: 5
    function: thread1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: a45efd50-2c6a-4102-af06-5b0b169af6c4
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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: 337ccc78-d8d1-40ff-ba2e-322625ae25f8
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 138
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e71be0d-9d65-4c71-a760-602b4361b009
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 52
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e3e0c1b9-a4be-44c8-b543-4addbf3cbdc8
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 90
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d3412d38-1a3b-4ed4-a7d1-7de48811bbb2
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 112
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e91fee33-0d2c-49ce-b4aa-19cf59e4d084
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 69
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 35cf2684-0da0-46e3-913e-35d21484435f
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 115
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 97448dcb-41af-4050-a8c6-2cb08bd8374a
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 113
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6dae77ca-9f1a-4f6f-865d-d0bbccd48afa
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 79
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b6e47eb7-49b4-4743-924e-6e6c35aa5c31
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 76
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 95618c46-4cbe-4ea4-bd24-a206d29da735
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 77
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3bfc64fd-c168-4bc6-b770-251ae868bd05
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 71
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b399f570-aac3-428a-8285-7b7b88a18e08
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 94
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4118f224-6b1c-41d5-a7c1-5c3bdbbec23b
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 86
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e49eafc-c488-4477-91ee-8b2b1f9eade0
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 97
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f512d771-5cc6-450a-a3dc-1a415059fdfe
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 108
    column: 5
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d811b984-f7cc-4deb-819d-5ded55079ff9
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 60
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ad8ff4b8-5dac-447f-bd97-271fbc6e3011
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 95
    column: 5
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2d9c6cdd-4f40-463e-b4c8-c0175564b6b6
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 50
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d4890948-7c09-4a7f-a67a-e2c285b24ddd
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 104
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3d6c5276-819e-4522-82db-5b0e910d6c03
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 67
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3b47dbeb-7d37-42aa-8996-e2bdacd083bd
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 88
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72c1db11-12fc-4f74-94d3-56c7822c426c
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 106
    column: 3
    function: thread4
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 53fa5e6f-a421-4a20-8d17-46f440655263
    creation_time: 2024-04-25T07:43:18Z
    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/popl20-more-buffer-mult2.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/popl20-more-buffer-mult2.wvr.c: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
      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/popl20-more-buffer-mult2.wvr.c
    file_hash: dbff9cba9b3794b18d55ca52c1abf6279404a7b220f91d79730a04b586f9ee44
    line: 48
    column: 3
    function: thread1
