- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b46fbcaf-84cc-49e9-a107-78d26cd2a32a
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb9db4ca-ba8a-419f-b18c-3e4a4607d5f8
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 710
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4266f01f-7a2b-42eb-afa0-9ab274c5b7f3
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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: c92487c9-f393-47ee-94e0-82db0a91b2c5
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 702
    column: 113
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4fc8c2c-5e98-416c-99ce-b2e5d0c835cb
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 712
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a7ad854a-8d41-4eb4-b564-e0a44fa9572c
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 711
    column: 8
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: d2664bf3-c72b-420a-a54f-7ad40d419371
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex1_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 838eb3ac-e612-41aa-a9d9-8251dd5751aa
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex1_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 701
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e762165f-8159-4025-b366-103d3b859afb
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 702
    column: 157
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f2f8efbd-27b1-4346-ad2e-dc72d9a54843
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 702
    column: 13
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 231896e7-8644-44cd-ad91-538ad5f08fd0
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 711
    column: 73
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 10a71270-4dfd-46ef-805f-db16ae82c8e8
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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: 277c674a-a059-4f03-8d58-e0b5e638f9cd
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 709
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 37e0badc-c01b-4dd5-b976-2b0a3c1d0f4b
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex1_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 703
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d3c2c5bf-a9be-4cf0-ba63-fe53afdaa813
    creation_time: 2024-04-30T11:00:54Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-g3c38fabe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_45-escape_racing.i: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
      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_45-escape_racing.i
    file_hash: 4864acf28eb3fe42b4a237468061905eb474c41e1edb519c0790cee08cdc91bf
    line: 702
    column: 57
    function: t_fun
