- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: bd1a1384-adee-4bc6-961b-9b9e8f98f70b
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 3dd59f13-003a-48b0-b1a4-b08b49252402
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: b992028f-7e28-4d48-b20d-d6605628e047
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 3340f63d-3d17-42c0-9081-aa5245e9f850
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: cb6495cc-aa6b-4800-afd6-1685dcaa0221
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 33db94f5-4522-4996-b138-13fe81b4ac9c
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: ab3389b4-ede4-480a-a859-b25e11434051
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 5f1ddc9f-d7c5-4596-9fbf-74ae4d2caa7e
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 9f5cfc9d-a48e-4deb-82e1-23b871bae89a
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: e9dc683f-4190-4f69-b06d-634247683e9e
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: b50631af-e24b-4922-ab12-84c93afcbadd
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: f546235c-6c0a-4f5b-a949-d0541101369f
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: b09dd94d-48b5-45b5-8fa6-0d422fff5600
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 75c4fdfc-7e1a-4862-9136-bf158048901e
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: d442e984-281a-43a0-83c8-0e7f1103e5aa
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: cf410ed0-de69-41be-a6b5-1800ee7577cd
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 9d4eae68-95ca-4442-8ccd-1aac66dd250f
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: 78657446-67b2-4ff2-9fd6-83e5a142393b
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: c408206b-3c9f-47ba-9c42-24c6a6c77776
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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: c1479763-0c5c-4819-9979-ac7f34bf9886
    creation_time: 2024-04-30T09:37:52Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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
