- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6fddb46d-1486-42a3-a9a4-ffc44f958684
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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: 08a46bbc-2cc5-4546-b0e5-ed8d38971ad0
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3909
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42311911-4ed0-46cd-a5ed-c1c293a7934b
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3912
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b1b9d2d0-1798-4a02-8ffd-2af8091b56c9
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3907
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0dba016c-9641-444b-a85b-416cc46a1432
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3910
    column: 5
    function: my_callback
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: eb72a1e4-404f-4d7d-b6df-f0eef45cf04e
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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: 109ec49c-2862-454d-9749-9f61dcfffac9
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3933
    column: 2
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e6e1fb2d-ce58-4087-a4bc-97c54cc0798e
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3915
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 279867dc-5fda-469c-8e3f-b43c0f6a7f9a
    creation_time: 2024-04-25T07:37:51Z
    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/ldv-races/race-3_2-container_of-global.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-3_2-container_of-global.i: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
      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/ldv-races/race-3_2-container_of-global.i
    file_hash: 0b03aab73b78beaf1bb7c49b9c847245bb2e0f74d5ca4021b62d8afb0b1e5702
    line: 3913
    column: 5
    function: my_callback
