- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85f57257-e385-4221-acd9-c132c6659e3a
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 93083b3b-1dc7-430e-8875-de9b0f3dbb3e
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 718ce165-645f-49ea-8371-0b5f3580ec75
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 539f5d20-0161-4531-a050-1b4ee4f4678c
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 9252d043-4eed-4bd2-9398-ce4e423a03a6
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 968f6bbe-5de7-4d2d-9507-135925734552
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 754d4122-3f83-428c-b73c-3774f4dd2f12
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 3c16246e-6ab8-4392-9110-e7b4861ab9c5
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 324a1c71-2b77-4235-9ce3-f85a90acd524
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: bc6cb1e4-758b-46b4-863b-17e978253ddd
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 721556a3-6dff-4733-915d-8c6dc504ea6c
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 9a9b8ddc-72f1-40f5-9a36-a959cd78f25f
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: da5a5a97-6a08-412c-abb4-61174c742f33
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: a49e80b5-7a83-4459-96dc-c3e145679cfc
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 6d771f02-bb9e-49bf-8a0e-5afd7d51f61e
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 55bad1cd-da10-4573-98af-28732b8785df
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 507d4b04-caf7-42f0-815d-7c9e6c70a86a
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 3e69030f-dba0-4d1b-9187-9473f4b7b7a4
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 2b32681d-e51e-423d-9b18-2b3ad45ee1ea
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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: 8e727ee4-24da-4a06-908f-728efb9c975e
    creation_time: 2024-06-19T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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
