- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c6cc84f3-3dbb-4a62-8b0a-cbfaeec0e8f8
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 57bac112-bc2d-461c-aaef-01af74ccc47d
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 715
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 66fecdc8-7bfa-42b4-a6b3-7951ec2cea10
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 717
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: be742c5c-e181-47f3-8c04-e3afdff240cc
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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: c4668d97-a488-4d7d-af0c-7091b788106e
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 112
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 88c28c85-f060-4c53-b63d-69869012dfe4
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 703
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8a1bd1f7-e2f5-4622-9f95-4865830ece0c
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 704
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1499e5aa-a448-41fe-b9ae-537bfb307ab0
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 15
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6a28a096-e63d-462e-b6cc-f3e55b7333b5
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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: 02b967d8-7b87-4c75-955c-f822bdfcbc39
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 713
    column: 55
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0f7c97d9-fc52-46ec-b3e7-d8c3743bb74f
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 114
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bf2feb37-76d7-45e3-988b-ef40e677f1ad
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 58
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b72be0d2-5ce4-4099-9c5c-ec22dab172c4
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 157
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94520c0f-02f8-4781-b930-d87b0373f379
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 716
    column: 73
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 02b2185c-1629-4b6c-8c42-cbd0e7626a9b
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 707
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f4235f23-1e38-4b36-b4b4-dacf297edb68
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 701
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 904d67ff-bab6-49a4-ab94-c8b91be6058d
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c70efce5-ca19-4a34-a73a-d0399fd17c28
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 56
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b1eb4f29-ea31-4eac-bfa5-d8348fdfdf03
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 706
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7313c9e3-65e1-4440-95d2-b48922ca76b7
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 700
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f2a28095-fdc0-4559-9c40-13491b749a35
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 155
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fce50ac8-3d30-4f59-b798-dd14a2b4ebb9
    creation_time: 2024-06-18T15:00:05Z
    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_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 716
    column: 8
    function: main
