- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d671c0f-8112-4266-a02a-ba9b5625d26e
    creation_time: 2024-04-25T07:32:39Z
    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/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 || ((0 <= block && block <= 1) && (block == 0 || block
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e7d4a74-a0e7-4b5d-99b2-ad461166202a
    creation_time: 2024-04-25T07:32:39Z
    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/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 || ((0 <= block && block <= 1) && (block == 0 || block
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a555770f-ab48-4607-9881-8b83aaca1b72
    creation_time: 2024-04-25T07:32:39Z
    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/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 || ((0 <= inode && inode <= 1) && (inode == 0 || inode
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 968a1bfb-7939-4ee1-af5f-00b6e03c3db1
    creation_time: 2024-04-25T07:32:39Z
    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/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 || ((0 <= inode && inode <= 1) && (inode == 0 || inode
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 091a031d-e27f-4694-84b3-f896989756b1
    creation_time: 2024-04-25T07:32:39Z
    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/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 || ((0 <= busy && busy <= 1) && (busy == 0 || busy ==
      1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6909d60a-20fd-442c-823a-759227c7b9bf
    creation_time: 2024-04-25T07:32:39Z
    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/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 || ((0 <= busy && busy <= 1) && (busy == 0 || busy ==
      1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1b55fd23-1a1f-4f6d-a481-bb203e5fe795
    creation_time: 2024-04-25T07:32:39Z
    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/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: b4dcf426-1db4-4c75-8476-b85f8f3d0633
    creation_time: 2024-04-25T07:32:39Z
    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/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: 562c8c56-555f-44ad-8c9b-4b5143f5d927
    creation_time: 2024-04-25T07:32:39Z
    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/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: a45935be-aa7d-43c5-982e-5089dd4d29bf
    creation_time: 2024-04-25T07:32:39Z
    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/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: 9f18a56f-8ae8-4280-854a-b7b8909a5496
    creation_time: 2024-04-25T07:32:39Z
    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/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: 92eb5dd0-873d-4e31-b59e-3f0e21836301
    creation_time: 2024-04-25T07:32:39Z
    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/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: e041d0aa-3bb5-4654-b85e-7651c7e7d88e
    creation_time: 2024-04-25T07:32:39Z
    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/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: 8ac81852-994d-41c5-86be-7183120ced6f
    creation_time: 2024-04-25T07:32:39Z
    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/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: 50c7cedb-32c4-4aee-870b-a4be8816a026
    creation_time: 2024-04-25T07:32:39Z
    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/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: ab944dd6-40bd-4f7b-ba23-8990e134e348
    creation_time: 2024-04-25T07:32:39Z
    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/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
