- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 57175d50-c7d1-4fda-bae9-42bb6c044099
    creation_time: 2024-04-26T10:45:00Z
    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_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: 5b8bf4e9-2c30-42a8-b6a6-a94eeec20f59
    creation_time: 2024-04-26T10:45:00Z
    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_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: 7e936330-a414-490d-a0cd-658ee3edab17
    creation_time: 2024-04-26T10:45:00Z
    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_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: 7b6abdef-9ac4-49d2-9db3-eff9c8333266
    creation_time: 2024-04-26T10:45:00Z
    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_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: f786fe3d-fdc4-4208-a22c-88227370f31b
    creation_time: 2024-04-26T10:45:00Z
    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_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: 4b08f05e-690a-4ce5-99e0-dfd809241fe9
    creation_time: 2024-04-26T10:45:00Z
    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_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: 32347bda-318f-4eb6-a484-079120f45762
    creation_time: 2024-04-26T10:45:00Z
    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_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: 8ef1dd0e-939d-46a0-9e79-b7748b408c6f
    creation_time: 2024-04-26T10:45:00Z
    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_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: 32f66fe5-4c11-4cf0-90af-b248d859a02c
    creation_time: 2024-04-26T10:45:00Z
    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_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: 26df9a22-5804-44b5-9932-4c2f70c1d626
    creation_time: 2024-04-26T10:45:00Z
    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_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: 7f35012b-0789-4316-82cf-0c2d9bfc46ac
    creation_time: 2024-04-26T10:45:00Z
    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_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: 18780bde-6970-4c6a-a743-b381b8e3d8ed
    creation_time: 2024-04-26T10:45:00Z
    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_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: 3a45d42c-8590-45e9-a67f-c037933f983f
    creation_time: 2024-04-26T10:45:00Z
    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_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: 4fb8ba94-c89e-40da-b280-40855a4dc30a
    creation_time: 2024-04-26T10:45:00Z
    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_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: ce566eef-24ff-45bd-8baa-d67e1d43bad8
    creation_time: 2024-04-26T10:45:00Z
    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_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: c9168d55-05b3-4427-aedf-75b770b00c5a
    creation_time: 2024-04-26T10:45:00Z
    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_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: 653c4f26-a75d-42bf-a987-c4ac6d68ff01
    creation_time: 2024-04-26T10:45:00Z
    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_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: cf823442-0c16-4aac-a079-735757394185
    creation_time: 2024-04-26T10:45:00Z
    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_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: 4d4e9280-6f41-44a8-bcb2-d255f560b9e0
    creation_time: 2024-04-26T10:45:00Z
    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_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: 38cc8940-9cf9-4b0a-a14a-998c594fcdc3
    creation_time: 2024-04-26T10:45:00Z
    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_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
