- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68705ac0-cfb0-4b31-b22a-3434b6cb76de
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 762
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89131a4d-6b54-48df-bf4e-0fdf13f73a8e
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 763
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b28899e-f644-4c69-b59f-809dd2e8ed26
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 762
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag1 && flag1 <= 1) && (flag1 == 0 || flag1
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34554679-fdf3-4c26-8f20-7ce03261366e
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 763
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag1 && flag1 <= 1) && (flag1 == 0 || flag1
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 450c6025-3a6a-4dc9-a317-aa3120c185d6
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 762
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= turn && turn <= 1) && (turn == 0 || turn ==
      1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2004371-fe08-471b-a87d-4ac80772fd90
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 763
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= turn && turn <= 1) && (turn == 0 || turn ==
      1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c14d29d-bbfa-4fd1-9c5d-b9576ce388b9
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 762
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag2 && flag2 <= 1) && (flag2 == 0 || flag2
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce4da75d-2fc6-4b82-9270-0b4ee90c85a9
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 763
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag2 && flag2 <= 1) && (flag2 == 0 || flag2
      == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: a2236690-c091-469f-b3a6-8d7f379dd613
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cc859a6d-f4c4-4863-ace3-06e00159b6a0
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 747
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 014770af-d0f3-4999-8928-3d44331641e6
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 719
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0be2645e-44ec-4ad0-81ce-461b43f44c10
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 717
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f827e59b-026b-478e-862e-adda9420d3ec
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 748
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ffda4596-da5e-4aeb-a150-cc62bc03e316
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 726
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a2e551a6-a70b-41f5-b60c-754ca05d638f
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 720
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dd19823c-3f1f-4358-9e83-046ac468ffab
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 732
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e81b49d5-0e1a-49f9-8011-46b0e90581fd
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 715
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 81dab447-8e0b-4b4b-a76b-2bbc7c43be68
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 750
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 552646a9-2b6e-4b3b-aa5c-fc4ecb63b204
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 722
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1f2ef6ba-9793-4020-9a8f-794105d99c55
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 745
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fddbdf00-530c-4881-a097-ec4bc8d6da6a
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 704
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3777f45d-aabb-42bf-9472-88d496cafe21
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 707
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 30afac04-5d5d-444c-a832-e56a0c07a28f
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 740
    column: 5
    function: thr2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f03ee001-265f-4ed5-b71e-f2d98def7d58
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      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: 29f6c272-6260-4af4-b8a2-db08c8cbf762
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      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-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 761
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b68afde2-3630-4680-a500-9048d87ea092
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 754
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bd61c4e7-0582-4b46-8b0f-32a156dc60ce
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 709
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99befb29-ce52-4955-a4da-8995acdf8588
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 706
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 23913c67-7b4a-478c-9363-bf98e760effa
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 728
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2cd4f0e7-2e13-4c98-ae54-2e76f72a97c0
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 743
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fca2d74d-eb32-4502-aa71-ef491311cf48
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 741
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5b81d27f-f9da-4d9f-87fa-57dea61d89e5
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 737
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a0d99b6e-7bc2-4722-8d4c-25f106ddd6f5
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 734
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c4f94eb5-78b0-425b-823a-fdbfb8d296a5
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 738
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e56a71fc-eb83-40a7-ab68-2e0617dc910e
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 712
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6131b5cf-c59d-454f-941d-168eae053656
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 713
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 725c2a72-fb81-4b94-90e2-7783328c1a20
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 735
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 75b0347c-73d1-4259-be61-bc894a8d9599
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 710
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9fa2ee2e-97a1-45d8-9822-466b30699386
    creation_time: 2024-04-25T07:32:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--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-atomic/peterson.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/peterson.i
    file_hash: ee3d1a41e169e13d6fb9bc974b1d8f7c8de5421cb2dfbc7e3d9a400662188398
    line: 756
    column: 5
    function: thr2
