- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 74055268-c149-4563-905e-46beef558514
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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: 08f5e18a-8ce1-47c3-9096-59745ba02410
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3943
    column: 6
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2deede74-2bc6-4860-9462-f1dddf2659b5
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3906
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4ee34ced-f546-4761-89c4-895079b7f544
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3911
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 35693571-1313-4bc9-be41-19423ad5cd8a
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3932
    column: 5
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 16b9708d-3a04-4d88-96b1-990b50d61af3
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3909
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 69976fb0-a496-4058-9754-8d14b4dfd78d
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3941
    column: 6
    function: my_drv_probe
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 0e3ae698-a21a-493d-bfc6-79af99a8c3c7
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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: 798b3ba8-ed45-4a7d-96ef-a76362d8a5a5
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3905
    column: 2
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 17ef14fc-cc1a-47bf-b503-d926bfba29e2
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3938
    column: 6
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1304a0ce-c68f-46de-afe2-9eeb0bbac22a
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3912
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 300b5092-17e9-4532-ad77-a7dc39ec03b5
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3908
    column: 5
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 570be89d-35a7-4f3e-9198-08a99cb21bad
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3934
    column: 6
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ee17c497-a6ba-4df0-a68c-09937c47c5d3
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3940
    column: 6
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 939d7e09-7a1b-4908-b606-8873e02f9839
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3915
    column: 2
    function: my_callback
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e032cf13-0d46-4d97-9740-c3cfdcad737a
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3935
    column: 6
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5dc92d55-65bd-490c-b48b-ee718d581aa1
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3937
    column: 6
    function: my_drv_probe
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f1de54c6-cd79-40f0-a05b-4ccc768dedfb
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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: f4047d2f-515d-417b-af9a-808444fddf3c
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3929
    column: 2
    function: my_drv_probe
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2d9acc09-ae2f-4cf6-a662-31adffbe14af
    creation_time: 2024-04-30T10:02:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-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_3-container_of.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-races/race-2_3-container_of.i: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
      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_3-container_of.i
    file_hash: 11cd6df53312b6388eb67fa3ddad4ddfe9675663ccf0a1507d8b60fd9abceccc
    line: 3914
    column: 5
    function: my_callback
