- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61851b26-d0ae-403e-86f1-2a38790bb20a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 22bd400d-5c32-4ee5-836c-d6a2516bb7b1
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 434319e1-8dc2-4cef-ad78-2da5d01c217c
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: fa7404ca-48a1-4530-9f16-903971b0bffa
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 8aa35c07-1f00-4940-b68f-de1abdef695b
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 72cb2685-754f-4ca3-84e8-69f84373327d
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 73890383-64f5-4465-b116-1b217a9c42b2
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: d2bc137d-9a84-4f27-ab35-86959522e283
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: a105dc42-f31c-4090-827f-8416ac1f763f
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: dae099a0-9bd5-4dc2-8266-7ace6175ad4e
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 94f55ed1-4ad6-4976-9c13-b2ce05a3ca11
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 68fad4a4-24dc-4f9d-9682-fb973c749407
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 1d7827fb-73d6-4e61-b6a0-bd46266ac75c
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 22110f74-50cb-48b1-9859-526ff8fecbdb
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 4290f4ed-d038-4ae1-9321-8d8d49053a6d
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: c530fdbe-b7b3-4777-8013-df685fbbf252
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 96233e67-bc71-41b0-ba62-6cc6ad5db7f6
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 88d46a4a-ccc1-4d90-ad3f-2f147376e591
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 78496fd6-e253-4bed-8c47-5be415c32fda
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: f92c54d6-38ca-49b6-806c-8716665261fc
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 57246688-7fc7-4fd2-956e-82030eb8e089
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 418fdc7c-45f2-4417-b7c6-681eb2ba3a4d
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: ad3baf91-a2b4-4486-82af-984b3a4d172a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 19aad564-a6d8-4c9f-818e-2ec6db09e11a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: d81966f6-9dd8-4996-9841-13661148f390
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 98c65ea7-d49a-4bdf-a36d-9f50126c2462
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: cca82167-f099-4453-ac5d-096e51188d89
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: b166c6b7-aa8d-47c7-a355-aa1ead150c4b
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 72e477d9-be1f-420d-b650-99d55f13b584
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 8d7a5c64-a6f2-4d01-b751-0487020c396a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 687fdc27-bb4a-4d9b-81d7-07e6c6241c9f
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: f39aa378-094b-49c0-a43a-d6191bf0128a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 576238d1-3f9b-4798-8bcc-75c26156349b
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 6eaab31d-384c-4f6d-becc-fa38f95dd569
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 11df53d3-72cd-4f36-b45f-bcf591761965
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 1e32f05c-e81e-4d80-a3ac-884a1db37d7b
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: fa276b7c-4968-446d-a8f3-8a3fc1baffec
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: fbcf9f4a-b709-4af3-b7d7-f92fac005a96
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 347fde34-bc56-497a-b0ec-c0fab23399f4
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: c23fa9fb-9ebb-4206-ada3-0e3b09fe1a11
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: a0648b38-f275-433f-894e-ca054ac1942b
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: a1dd5c6e-2c45-47b4-b104-cabfa417fa54
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 9ee0e445-6825-4081-935a-1a1e3472a663
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 05feb800-1d62-49e2-a6ed-12c750c2f876
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: c8a66ba1-35b0-4bbc-9963-36be8769762d
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: ddf27e5d-ee28-4523-9b98-ae188fd5882a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 45ccad03-a7a1-4695-92cc-ea77758819ac
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: c4024d16-182f-4e8c-8965-010087303318
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: baa8a3db-de0a-4e1b-ba82-079a43e0250a
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: bde35d30-b23e-4a45-be63-f0619596a690
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: b44b5003-b927-495d-90eb-bdb46de554be
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: ff4f7631-5737-49b4-b838-513dd0bfa0c6
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 3311d764-6d89-43b7-a04e-203186eb2a80
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 42856c10-7367-434e-bc3b-46deb6db7c59
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: f23735c5-8f12-4fdb-a935-04738f35ca42
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 1f54023d-a2db-4e1a-af57-34ba3d8e6a0f
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 9f553d05-0e30-4591-81a3-49ca9703d8a8
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 80ca05cf-3d27-4b2b-ac37-016998720e7f
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 0379f75a-6e45-479d-ba8e-91d4c4c85489
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 797a79b4-1fcc-449e-877d-8ab2a77d6db7
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: d027ea81-b66f-482c-b003-26f8efa2d887
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: af7737e6-3c7c-45ef-a7e3-379f15b15fc8
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: af24b4e1-bdc9-4227-b907-99c81aa72c17
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: fc1628a3-1a35-43a1-a39f-1e627a13ae9c
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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: 5fe62834-ed69-4b6b-bc91-29b8f22ec746
    creation_time: 2024-04-29T10:56:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/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
