- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: ccb28695-d8de-4b00-84ad-68c785ac4e1c
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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: 65ae472f-bb91-4fcb-b661-5c6cfa819a76
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 730
    column: 9
    function: BCSP_IoDecrement
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 44f79365-125d-4b7a-ab33-a51e738c8871
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 748
    column: 5
    function: BCSP_PnpStop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aabb593a-10df-46f6-81d9-51ef195bfef4
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 737
    column: 5
    function: BCSP_PnpAdd
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4bb7533e-445e-4b2c-9815-6fb715061321
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 750
    column: 5
    function: BCSP_PnpStop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8ec11d3d-1526-40d7-8fcd-ce7bde58901b
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 708
    column: 9
    function: BCSP_IoIncrement
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 30b15332-9438-4d3c-bbbd-47c45ffe3a36
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 718
    column: 5
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eafdd6b0-21ae-41e3-8a06-d1ce6a0d2cbc
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 728
    column: 9
    function: BCSP_IoDecrement
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1c73829-dbe4-4b62-b898-cdcdea1fc2dc
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 704
    column: 5
    function: BCSP_IoIncrement
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4ad70609-a7d5-446a-a0b6-9f482e11a593
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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: f1de2b92-3e57-4fd7-ac60-ace21d59ed81
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 761
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1d386c81-03a3-4b9d-bd96-4f39ce9d909b
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 713
    column: 9
    function: BCSP_IoIncrement
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c5cf4d5c-a486-4786-8cef-9a0537ee6a60
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 746
    column: 5
    function: BCSP_PnpStop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1837e6a2-0361-4af1-8c2d-b7ed27a212f5
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 752
    column: 5
    function: BCSP_PnpStop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 93007073-abc2-4d9b-833c-14897e7d0607
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 752
    column: 45
    function: BCSP_PnpStop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: efdae1c8-7623-48d6-b85a-26d31dacb8ca
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 702
    column: 5
    function: BCSP_IoIncrement
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 125227a3-1e4b-4967-b23d-05d8321def0f
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 721
    column: 5
    function: dec
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d13e071d-2e1d-44b1-90ec-e70b54de0d82
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 744
    column: 5
    function: BCSP_PnpStop
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3c826979-4621-4dea-a8da-400371c45882
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 737
    column: 64
    function: BCSP_PnpAdd
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0618da52-618a-4c0a-970d-81fee1b6ebf3
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 711
    column: 9
    function: BCSP_IoIncrement
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b5a34bb5-97cb-402c-98f4-97b3182d5d48
    creation_time: 2024-04-25T07:37:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-lit/qw2004-2b.i: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
      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/pthread-lit/qw2004-2b.i
    file_hash: f17f6182d2330561fe6717b6a061d0dded698483f9e32b37a3b36e1144855a29
    line: 710
    column: 9
    function: BCSP_IoIncrement
