- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43cb0f3d-c3e1-46f1-b606-af202ae862da
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (m_busy_locked || (busy == 0 || busy == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64106268-44c8-49ef-9e59-d7105aad218d
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (m_busy_locked || (busy == 0 || busy == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 161b8899-a554-4ced-87ab-6c4c608bccd5
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (busy == 0 || busy == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 886d9294-d0c0-4bcd-b33d-034172138045
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (busy == 0 || busy == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44ebc0de-707e-4a7b-9406-bf5526319f2d
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (m_inode_locked || ((busy == 0 || busy == 1) && (inode
      == 0 || inode == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40319b9c-5140-48a9-af59-3281584f235d
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (m_inode_locked || ((busy == 0 || busy == 1) && (inode
      == 0 || inode == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27b81411-5a64-4893-a6fc-718d2594094f
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (inode == 0 || inode == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3aaadca-de8f-4eb6-ab2d-5785e9afda1d
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (inode == 0 || inode == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1aa22dd-d578-44b3-83c2-d434043ce454
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (block == 0 || block == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6de56b04-9f61-458d-8081-1c45bf65f32a
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (block == 0 || block == 1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 697a704c-0081-4012-b4d2-32fc561a1195
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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: fcf84776-f47c-4686-9e58-efe0831afa32
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      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/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 720
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 906d9b8b-fcdc-45f1-a7b3-3b9a561fb2b2
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_busy_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 266a1b42-5002-40b8-a58a-fc148ee264bf
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_busy_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 698
    column: 5
    function: allocator
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f404d38-56ea-4175-baa5-20e7a74ddeec
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_busy_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 707
    column: 3
    function: de_allocator
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 424d0b11-53ac-40f6-bcf0-ee147e83ecd2
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_busy_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 696
    column: 5
    function: allocator
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6e5dbefd-3f94-45f4-8312-d7d88e38f6e2
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_busy_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 712
    column: 3
    function: de_allocator
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: daa42389-2a0f-4cbf-86fc-fff6d2e1e05f
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_inode_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 31c4c183-40ce-4d40-9628-1d6ffc3aff3c
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_inode_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 703
    column: 3
    function: allocator
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c121efcb-49e8-45f3-b706-e887470ec930
    creation_time: 2024-07-04T11:53:21Z
    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-atomic/time_var_mutex.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_inode_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/time_var_mutex.i
    file_hash: 1985bb251db70a1c798d345be7e1671f9dcc6a359b969ca99d23e0003d9a3770
    line: 694
    column: 3
    function: allocator
