- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0387d50a-4546-4719-b596-ec18545fb991
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 735
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || (B_locked || (((-32768 <= g && -32768 <= h) && -999
      <= g) && -999 <= h))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65a983c8-6e73-418f-808c-f497afac4d89
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 735
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || (((-32768 <= g && -32768 <= h) && -1016
      <= h) && -999 <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17e7eb6e-4e16-483e-b316-d648f5c12baf
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 735
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || -968 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83dad792-1f94-41d6-800e-fb6c39afd230
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 735
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || (-32768 <= g && -999 <= g)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d43ea3c8-6d2e-4508-acd6-e2ec6c97d693
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 735
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || (-32768 <= h && -1016 <= h)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 826bcbd8-c839-4c39-9e53-466943a7aa59
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d6f4125c-46f5-4f19-b2d4-a0e3658d3699
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 741
    column: 5
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 10cfb2f1-2e02-4b0e-89ea-15fd9d6aa0d2
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      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: e36ab0aa-c4fe-4ffb-88ea-4682bfa356f8
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 734
    column: 5
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 37b62555-8132-4682-8460-567449860223
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1ca3232-2bb0-4bec-9ef8-b74b9f36ed5d
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 747
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1703a0ae-6386-49eb-90d2-e9ad834d3eef
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 725
    column: 5
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 4880db8a-1dc9-4818-ae45-d85bdfd72c4d
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3badfe6d-8a44-4480-80d3-f96b24f64af0
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 719
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 968ef9bf-936c-4e68-b97e-f6673c5f09f9
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 721
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2fa46303-32a2-45b8-a24d-9ce870546a56
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 743
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5c037981-2e31-42ed-a8ea-9ae91c807747
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 740
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3af81a27-3f0b-4e99-a0f2-92aa259c8411
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 744
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8c070c5-c12c-4e12-a477-7a092d7411be
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 736
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b20e4564-27cd-4bfb-a585-4659b88841fa
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 745
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0f7e4d88-5945-4fbf-a4c3-bd68b7461d66
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 726
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 370ed0c6-054b-4a4e-9fca-3cb37bf6c704
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 715
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2bb05202-71fd-4361-9d44-d9aa7c92bce3
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 735
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ceeb916d-348d-46c3-968d-59eacbbd766b
    creation_time: 2024-04-30T10:07:32Z
    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/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
        : 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_22-traces-write-centered-vs-meet-mutex_true_no-overflow.i
    file_hash: 6883737711af32a6a824eca7af237353e2fdaf7712a6b3c22083c0d47b565ee7
    line: 714
    column: 5
    function: t_fun
