- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: a92eeccb-1457-46c5-bfbc-b570218740f5
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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: 48701c28-c573-42d1-82ea-b3c09cf7c1f9
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 944
    column: 97
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3063fce3-cb22-4fc9-a248-1bac68a7af50
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 944
    column: 349
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b860aa38-4680-49d0-b59e-e31b7345b3a1
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 955
    column: 155
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c138cec4-d0e8-49e8-89d2-8e8d4170936b
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 955
    column: 207
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d95b092b-56d5-4c43-ace4-8d18941c777c
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 944
    column: 153
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 57b23190-7501-4512-b903-3630c06a6868
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 955
    column: 99
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 18ff0f53-d4de-424c-943e-cdf541ff3d31
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 955
    column: 47
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8d72775-8dc2-4809-b388-4247c7b0ce17
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 944
    column: 47
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1eddafed-4c7d-46ba-87ba-682f0a7d7dbc
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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: 4475ece8-92e6-45c3-b8c0-b1d9f6538475
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 953
    column: 55
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3107f030-c7e4-407e-ba46-c533b62354c8
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 944
    column: 203
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6dcfeed0-f3ac-4b7e-9b24-fac9a2f614df
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 955
    column: 355
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9ccedbdb-9738-402f-805e-4fd3a85967e4
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 944
    column: 277
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4e22b5c2-ecd7-421f-a2d8-d4762153d97e
    creation_time: 2024-07-04T11:40:22Z
    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_74-tricky_address1_racefree.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
      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_74-tricky_address1_racefree.i
    file_hash: 9a7db49c8892594e32a30fa9165fc3ad1a94911917cd8b63757bb8f24f04b536
    line: 955
    column: 281
    function: main
