- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5e8a418-aa3f-4ce4-8ad3-7413216f3b44
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= flag1 && flag1 <= 4) && flag1 <= 127) && ((((flag1
      == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc20d7c8-6f5f-45ea-be69-557a08fb283c
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= flag1 && flag1 <= 4) && flag1 <= 127) && ((((flag1
      == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a54dbbe-f327-41bf-ab35-ec6691a44e20
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75a959ac-a7ac-4350-bc2e-c758497ed139
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6412900-9917-4299-a750-f8c09b3e8caf
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= flag2 && flag2 <= 4) && flag2 <= 127) && ((((flag2
      == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6792145d-5ea7-4d16-baf5-4cdd2e9c912b
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= flag2 && flag2 <= 4) && flag2 <= 127) && ((((flag2
      == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddfe1aaf-57de-43e3-94e4-bc0777543798
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 819
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((0 <= flag1 &&
      0 <= flag2) && flag1 <= 4) && flag1 <= 127) && flag2 <= 4) && flag2 <= 127)
      && ((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4))
      && ((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f1383fc-3884-405d-ab67-0fd25bfc2d60
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 820
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((0 <= flag1 &&
      0 <= flag2) && flag1 <= 4) && flag1 <= 127) && flag2 <= 4) && flag2 <= 127)
      && ((((flag1 == 0 || flag1 == 1) || flag1 == 2) || flag1 == 3) || flag1 == 4))
      && ((((flag2 == 0 || flag2 == 1) || flag2 == 2) || flag2 == 3) || flag2 == 4)))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: be90b374-ea3e-4295-b530-5b02e24cd729
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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: 255fc621-c132-4ba2-ac5c-588c40baa3aa
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 733
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7498fd6d-3c54-403e-9832-1c2316bc0273
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 807
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cbeccadd-06ab-47a6-bc6e-70d0f8b31e7c
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 750
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf6b073e-f8dd-4cab-b311-2b76f89616f0
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 742
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 399a1b2a-f0db-4c56-8521-1152a97061ae
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 752
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8e28c32-7177-4327-b1cc-c32e9122e693
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 799
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: defbcdb5-7c2d-46c6-a1de-1f63cf3f415c
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 710
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d1d1e354-db6c-4e94-935f-63537cada544
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 797
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 345a9bd9-8860-4dbf-9070-fa9fad5de168
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 787
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe7f694e-4832-446f-9cfe-fe269ffec992
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 783
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b44f9a63-4ad0-4044-a276-436260cd693b
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 730
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: baf30639-8e25-4b5f-ac9c-4cc56e08b025
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 728
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9740dcb7-8e8b-4b4b-ab49-166bdb0c7c0e
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 767
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b7b8320d-bd61-4a78-a0af-39a85f1390d1
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 769
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a190f808-1bbc-4b7b-a0d3-b55586d2ecc1
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 785
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 866b2577-cbd7-4733-b369-07e40834dd97
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 712
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0a45f01b-a2d2-4424-9a32-373006f3f446
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 809
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f220963d-5570-4367-b9ea-766c26969658
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 740
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 38acbb4c-9bf8-4edb-8cdb-f7d7fb4e1f16
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 792
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0168c39-8d0e-4253-83b1-cedc1ac0e6ae
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 773
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0cd7f9d-e9bb-4f5c-9d24-0fae811cd78e
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 726
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9f31217d-b429-4881-89b7-17f184c3bfd7
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 736
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4e98c842-4e4d-4e20-bb58-b9a89a9c7d0a
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 708
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9123b1c6-455b-4863-9e08-79e0b8ab6470
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 813
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2c6f549e-2adc-4dac-abd6-6893e2accf34
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 774
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a8e4617-427c-4416-b5a0-8ec1f0e63837
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 805
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5201a268-ff3e-4ae0-850d-79bfe961b844
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 716
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: beefab00-4a57-44a9-9d45-d794876880bf
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 717
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6082947c-c461-4da2-97a8-4cd657d95281
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 811
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 70aabd19-ff7f-4c77-9697-f5e93cd8f632
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 723
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 91fd63ee-c0c9-4f49-9b89-4b0f1c4f2a8a
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 762
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1ba19fd5-610b-474a-94c8-d25754ef0e5e
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 771
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5d8704e7-9871-403e-80ee-dffa205eefce
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 721
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 56c3c889-109d-4a03-9b27-4d996c9b39be
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 760
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 27a32d18-c44b-4ec5-896a-3f928182885c
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 754
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cbb5cb04-5dba-4eaf-89c0-641bd72885cd
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 781
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 694ee982-812a-4090-88c4-0cae49a35b32
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 776
    column: 5
    function: thr2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1c6dde69-8e3b-4b57-a8b5-b85b4dab3cd9
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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: 8a4476ec-248f-4e69-8c32-e138700c8f06
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 818
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bd68e5ba-3c31-49ce-9b60-4c49a1c7011a
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 714
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 797b9d5b-e2a2-4a05-accf-65bf7a0221d0
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 719
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e5f77810-a8cb-4401-9992-dc83123dde79
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 703
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7f909d37-f470-42a9-a596-411db93ca74d
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 748
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 514cf571-5942-405c-8a69-e21ef833fac6
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 756
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8b0258f2-9660-4d83-a365-6c0aa5eb876d
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 706
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6bb1357c-3a0a-4c5e-9dbc-73cc7515f857
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 746
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 294cfac5-3196-49a8-a485-09e0600c5c53
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 735
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9edd33d2-9a94-4b6c-914a-3e823ccd13f6
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 795
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0913dc12-4ecb-4201-a01d-589ab9904961
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 738
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 511f8c6c-225a-4ded-8e66-c47fb5e3094e
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 780
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9acbc8ac-894d-4305-acec-7b6b50f12011
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 790
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: befcfa2d-243c-408b-b680-5a2bd59a6dac
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 705
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f4eaecf2-a43e-4f57-bc63-bbaf19bfca20
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 724
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0b4e0988-fcc1-4186-8c7c-ddff4a1f1891
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 765
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a339a6d7-e85e-43e4-8e6e-08be58877e26
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 793
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 157f2aec-4dad-43db-b4bc-668d46e2f05c
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 763
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a018b56d-46bf-4d69-80c1-cf921ad81cb0
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 778
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d3f899d-3953-4419-bb26-df0b8a6ac1e1
    creation_time: 2024-04-26T10:36:42Z
    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/pthread-atomic/szymanski.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/szymanski.i: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
      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-atomic/szymanski.i
    file_hash: bc84ca2197caec735a8480f9d61b820c686ed9ae52711f2c7500999694c2ad40
    line: 803
    column: 5
    function: thr2
