- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35b43ff0-0491-4684-bbc7-90bc3a242b76
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 793
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((0 <= flag1 &&
      0 <= flag2) && 0 <= turn) && flag1 <= 1) && flag2 <= 1) && turn <= 1) && (flag1
      == 0 || flag1 == 1)) && (flag2 == 0 || flag2 == 1)) && (turn == 0 || turn ==
      1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60c0702a-668c-4410-8af4-e9fdfdd94e3a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 794
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((0 <= flag1 &&
      0 <= flag2) && 0 <= turn) && flag1 <= 1) && flag2 <= 1) && turn <= 1) && (flag1
      == 0 || flag1 == 1)) && (flag2 == 0 || flag2 == 1)) && (turn == 0 || turn ==
      1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 163645b5-01b3-4d44-aeeb-7be46cefd714
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 793
    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: bc2d322c-6179-4274-9d91-0ffd181671af
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 794
    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: 503fce18-7263-449e-9cc4-45bb8eae787a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 793
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag2 && flag2 <= 1) && (flag2 == 0 || flag2
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46921843-3ca8-4a4d-a229-9d4cd5fb531f
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 794
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag2 && flag2 <= 1) && (flag2 == 0 || flag2
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92e1a97e-b24f-4177-9111-12462b8dcc04
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 793
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= turn && turn <= 1) && (turn == 0 || turn ==
      1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70050de3-33b6-45a6-8b0a-ad5fb17c151a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 794
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= turn && turn <= 1) && (turn == 0 || turn ==
      1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ccf8f0a-c9c7-42a0-ad87-a78ffa3aa26f
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 793
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag1 && flag1 <= 1) && (flag1 == 0 || flag1
      == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a38756de-13d0-4d18-8e74-8e9d65613343
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 794
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= flag1 && flag1 <= 1) && (flag1 == 0 || flag1
      == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6ab12d1e-59eb-4435-8c98-065ca44325a3
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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: 9f2eac41-97a9-4bdc-a603-39f563c1764b
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 758
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e03a651b-07c0-4436-841f-3287779c3ec6
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 726
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e6ae4fbd-f9b9-426e-bad8-15d5023d0fe0
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 728
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b484e415-e1fb-49c0-9ca8-bb3b2fc6c568
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 767
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c134a0eb-032d-4fd1-928e-67be196d32e7
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 783
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b4ae800e-26dd-49bf-9a3a-78ce700d74b8
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 769
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 417f2299-9ae5-4654-8548-929236f3ff99
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 773
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 82d5ad8d-6f1f-4cb6-8a15-a28709594d11
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 786
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4d0c5d6a-7775-4129-b2f6-bd6e8587f9c0
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 763
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09d083a0-8547-4111-b516-0bf0957eab8b
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 765
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d355d516-36c2-4f1a-abcd-171b929f1b9e
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 721
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2bb15f56-f01f-4c74-bdbc-b7a3497175b5
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 708
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 933d991f-26cc-4688-be7e-2d287d469f15
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 740
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 68f56c1f-79e2-4a53-989f-91c810a4df8f
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 719
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 842558b8-2596-4af8-8d75-6a207ee28ba8
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 742
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2f2a1090-0d17-4a2a-919a-fa6eee3d7697
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 732
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 37a99dbd-b239-4cbe-9ad1-1c38ee77515a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 743
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bee66b44-b05d-4185-b00c-388e9ba6f177
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 722
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a3989702-72f6-40da-b3e3-c9401c56c854
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 715
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4301078f-0ebc-4a23-a83f-5eb2197c66d9
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 752
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fc5b0cfa-ca89-46ee-a119-b9951de5563d
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 745
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0789202b-1255-47e4-9e2e-a476b3ab5b04
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 749
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 234b01d8-221c-471a-b9ba-245ad34ebfb2
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 756
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8a5f84a-7ac2-4945-853e-eb533b0814ed
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 762
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4c9e7d1f-db31-470b-8bcf-d5cacdb0193a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 775
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 575e65a8-c1f9-479a-91ad-bdcb207f316a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 711
    column: 5
    function: thr1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8ff1f388-a36b-4314-bdac-3b5614e20d77
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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: 5dbb09f8-1aa6-4c19-a742-5aca843d593b
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 792
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1c83d69d-7b00-4811-a626-7b6a90e84aa2
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 724
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 156828fd-5a24-428c-980f-8ef4324e76d1
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 734
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6318592b-6aaf-4b15-b10b-cddffe00c118
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 784
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2816edd3-1033-4e7a-a418-defe9491d309
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 713
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6134e7ff-e8c6-4a23-aa9c-be59bbec362d
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 760
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9b5476cf-e91c-4d14-bbc0-16c48e28c3ca
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 781
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d48c8d0e-e6d0-4df8-b567-3857ac37ad60
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 754
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72fe7dcc-e236-43b9-be63-ceb8cb40ce4a
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 710
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 41f8d29a-e200-44b2-8dec-02323db01984
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 730
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bdc5052d-1e30-4531-be32-f2a257d8e9fd
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 717
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4e911775-1e4d-4487-95fb-59e1927f9bcd
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 771
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 225c2cec-fcab-4ed8-b1c2-5f193d9b3097
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 777
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4d20fcaa-522a-4bc1-9da1-53dea3d7f284
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 736
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a45e4444-5df0-4aba-bf2b-06a1883dee2c
    creation_time: 2024-04-29T11:43:30Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/dekker.i: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
      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/dekker.i
    file_hash: 1b6ef65da122b5f043dc58aac5c98a5417eca7613b00ec724ef2626b8a50d79f
    line: 751
    column: 5
    function: thr2
