- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7dba4fa5-9c07-49ea-9ca0-a51a264003c5
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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: 49bbb5e3-9a87-4298-a13c-5e9ba611a3f4
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3945
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 13165255-095b-4a01-970a-2c8ad071fc31
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3946
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1ecb0203-1c8f-444f-baa0-f2b70e4aaae7
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3906
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 662087fe-264b-40d9-9d55-620a32bd2c47
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3951
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ebf92f0f-4efc-4a8c-830e-262f9a4717c0
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3911
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 038f3fd7-670a-44e7-a1bc-3456c632ced3
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3909
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c542146f-79af-4a73-bd14-f31b99c9a3bf
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3948
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7efe5ebb-fbdc-4691-a4cc-2157f44ab56e
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3943
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 228b0146-e40d-4650-8fa2-4f8364a1eed5
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: data_lock_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ccc1ce1d-6b13-4ead-8dbb-a43cd2b55dbe
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: data_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3905
    column: 2
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 306dbd0c-08db-4af3-ad35-b90d6f387d37
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3940
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d2541072-00bc-4088-a851-34cdbac00165
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3949
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d578c404-ae42-48d2-9683-45f6b55024dc
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3912
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bf9ecaaf-d909-494c-b8d7-cd15c3348bfb
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3908
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 63d87b27-391e-4fc9-80a2-0b0ab6d5bb90
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3942
    column: 5
    function: my_drv_disconnect
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 982cc099-42fd-44f7-a4ef-1891ce3492f7
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: data_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3915
    column: 2
    function: my_callback
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5e493f45-09e4-4491-88a3-bb624d648312
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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: eec394f2-497f-4397-9f54-7ce640086510
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3929
    column: 2
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 18d6e858-cb87-4665-96da-60670b8e53ee
    creation_time: 2024-04-26T10:45:01Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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-2_5-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_5-container_of.i: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
      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-2_5-container_of.i
    file_hash: 3c93f158b090fed5438343046820ebde54acd91fe2fe757fc7dc28475dc42a7e
    line: 3914
    column: 5
    function: my_callback
