- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5dc4bf14-20d3-4f63-95d4-3bba48f94ae8
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 192ecbd8-7317-487f-977c-0ca76f23bf93
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 692
    column: 2
    function: inc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3602fd44-866d-48fc-b7af-4945ef2b6346
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 706
    column: 2
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9d2e3aa9-e4d6-4009-bdac-6604898b8d9f
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 713
    column: 3
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb3bc1f8-b0aa-4146-a998-80b1bb48c07a
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 699
    column: 3
    function: inc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0e1e422-66bd-4b06-9fad-4c2f2f44d314
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 700
    column: 4
    function: inc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed6e8ab0-4e0d-4c12-96b9-12c1f45f4b71
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 714
    column: 4
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76b9004e-a484-464a-83e3-7750c068601c
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 708
    column: 3
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94eda8cc-4125-49c2-af4e-ee77ed9db3d9
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 714
    column: 108
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4ea05d2b-e151-4e1b-945a-c78446f97e5f
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 694
    column: 3
    function: inc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 64768ab8-339b-4e42-8c27-69c935d07213
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 700
    column: 108
    function: inc
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 11fee12b-e3a7-47b0-a488-586c59280287
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      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: 06860e73-75c5-4ad1-98be-dea97eafcbda
    creation_time: 2024-04-29T11:43:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-ext/03_incdec-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/03_incdec-pthread.i: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
      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-ext/03_incdec-pthread.i
    file_hash: 7f19dc7b6c5c71a67d9914faaf2a1157355ecf0e14b05edf8c2541b2f25a5ffb
    line: 726
    column: 13
    function: main
