- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 58de3d38-30ba-4f5b-aa7b-65a942ea9690
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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: e490ed5d-4a34-4531-8554-2cad957f7a09
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1015
    column: 3
    function: take
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a03734e-a85f-4030-afcc-650b55e1380f
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1022
    column: 3
    function: insert
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9db9b08a-d4f1-47df-86e7-967331471a0a
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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: 3ea84945-b070-4cf3-85ca-996bd3e4da31
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1037
    column: 97
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 03ec13f8-ed45-48f4-9507-08960600a7db
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1026
    column: 3
    function: insert
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d25218cc-2224-4083-960a-4de0d120abc1
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1037
    column: 277
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6be89475-d803-4993-a62b-d6ae0d840364
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1037
    column: 47
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 665ae0d2-5f4b-48d9-888b-91f40dc6097d
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1018
    column: 3
    function: take
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 85c8226b-270a-42a8-860a-bbf53b94e5db
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1037
    column: 349
    function: t2_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: d569cde6-e71f-464a-821f-031c867e9840
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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: 4af03f3a-61b9-47a3-8ae6-0376c704974c
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1042
    column: 56
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9201b11b-9c74-41a1-870c-ee9c3468e01c
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1037
    column: 153
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99efc7cc-1c8c-4b14-80da-a3731961ca0f
    creation_time: 2024-06-18T15:01:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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_81-list_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_81-list_racing.i: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
      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_81-list_racing.i
    file_hash: 3de6ec2acea23c0ab47fbc2e02ad0931145060ca78b80531ef692b3505f9553b
    line: 1037
    column: 203
    function: t2_fun
