- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1625f0d7-9f95-4f92-a9ad-aac150f6012e
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      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: 1d16c8e8-682e-415a-9d7c-bfbdeccf9130
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      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/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1310
    column: 13
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 50592f5f-3262-40ab-a6b1-f35c0dcb16b0
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m563103013_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c3f665db-c054-47e9-95a4-70293c46af15
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m563103013_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1267
    column: 5
    function: funcB
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f414287-7372-4917-81a8-2ebb44e45aca
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m563103013_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1269
    column: 5
    function: funcB
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: cc3c8459-fa62-4676-8059-48f126aab6f8
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a88b8e56-7519-49de-95c6-ad768f12190e
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1249
    column: 5
    function: funcA
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 19cbf93a-24d1-4d0c-ad28-9055bd2c500c
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1262
    column: 9
    function: funcB
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 997d2fef-e0d7-4c0d-a321-1debf824d572
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1260
    column: 5
    function: funcB
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 095277ff-bdf0-4a0e-a027-0d34d478763f
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1248
    column: 5
    function: funcA
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d109323e-ae77-49e2-8150-d9675cb1f015
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1246
    column: 5
    function: funcA
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 785b26e3-7792-4865-9d3a-20fb47c78ff1
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1251
    column: 5
    function: funcA
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d43671c2-207a-4ab0-8ee1-5560dc851e34
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m563103013_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1252
    column: 5
    function: funcA
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76abd633-d550-40af-b573-52e329e2237b
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      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/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1304
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: df83a028-01d9-4a92-bcee-b48b80385d9f
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m563103013_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1254
    column: 5
    function: funcA
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1259ced6-d6c4-4d52-9d94-ed9841015aa7
    creation_time: 2024-07-04T11:53:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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/pthread/twostage_3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: alloc_m527474924_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
    file_hash: 1032ef3fe166161226ca7e81ea27802cfc3f516ad1e4b45c387461fe1ddeccf8
    line: 1266
    column: 5
    function: funcB
