- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7e798159-7b0e-4bd0-8d4e-6f65c672c6c0
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aeea2791-3680-4fc2-b713-a2d99e0211c3
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1046
    column: 349
    function: t3_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9dc5c43a-1eb0-4c58-8392-5de917e7863e
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: list_mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8c821732-f279-484c-9abd-65b52ab300e9
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: list_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1022
    column: 3
    function: insert
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6eb2f64b-1d28-41cb-bcca-4051d7aae675
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5b0e3e89-d8ec-4b1e-8222-e45649fd1380
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1047
    column: 3
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0e47ae2-c399-4bf9-9784-610f21213627
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1039
    column: 349
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3f0906a2-7bc0-40be-98c5-d018e692ce78
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1039
    column: 97
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5aefc5a7-894c-4c5f-8927-5c81e856230a
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: list_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1018
    column: 3
    function: take
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 413d60ec-022b-413b-8e56-f7dd9c488f5f
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1039
    column: 277
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 27e3c582-262e-4677-bd46-01199d7b075c
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1046
    column: 277
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f4dce963-a594-4aa7-ae73-a047d8e62f60
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1046
    column: 97
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cee9a4e1-281b-47a7-bc35-ea359b56a5cd
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1046
    column: 203
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e476518d-3965-413a-a4cf-a3f1a0eeda6a
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1039
    column: 153
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 224588d1-227a-4f3f-866f-0592fcf6304c
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: list_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1015
    column: 3
    function: take
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: da591200-5285-4ece-b1d1-3b04935c1bc9
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1039
    column: 203
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 535d1563-98e0-4014-99b2-e848c116677b
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: list_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1026
    column: 3
    function: insert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 22eb4bb9-7383-4e8b-91ed-6b285a97acac
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1046
    column: 47
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 20b3902a-7f3c-46d3-8f7f-36dd60ef3169
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1039
    column: 47
    function: t2_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 15405764-ea42-447d-865e-54ae0c1aab35
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      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: 7036281e-6ed2-4441-aee1-cb1613c3a2bd
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      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/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1053
    column: 56
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b55e1fef-dca0-4b84-b1f8-75ff54a699a4
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1045
    column: 3
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eae52f65-4241-49ef-b5ea-67c84a63f44b
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1046
    column: 153
    function: t3_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 84c61680-d837-4d7c-8e9c-2bdc1f6b1e88
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 797dc139-275a-47a1-b7f2-2f65029e5ed4
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1038
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2fa3c11f-258d-4c6f-9004-e07e18bf188a
    creation_time: 2024-07-04T11:41:00Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/goblint-regression/28-race_reach_84-list2_racing2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_84-list2_racing2.i
    file_hash: f70125267ee7251a74a40ef1ba0ea3ced14d0fe45e7a9ea5a666e1eecab0c01c
    line: 1040
    column: 3
    function: t2_fun
