- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e93d353a-9f1d-4b14-be0a-751a623c34dc
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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 || -999 <= g'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5deda3ad-0b3a-400c-80bd-36d0df9727dd
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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 || -1016 <= h'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c05c583-68fa-4d80-b970-9c34d3bfcbd0
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 01b0e3eb-7ada-445c-98fd-0c8e790c84f0
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 021593b2-027e-4cbc-a66e-37f63d71b5eb
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: f912cdb9-e617-4867-8bf8-c07bdfbf7866
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 18981879-b146-43db-bdf8-590c7f141e7b
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 573df61f-23b8-4a43-bf23-89d3bf2b9889
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 3b1809f7-aab3-463e-9681-9d518f6e808b
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: df06b69c-a214-408d-90a5-7f456a63d009
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 9c298520-b2ea-40c4-96f0-8c6c5afdb1bb
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: be53acbd-a352-4285-b36e-7d9bd8f1445c
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: b539e024-93e3-4147-9ea8-c0d1faa9e87f
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 023dad94-edcd-4dfe-9b9a-d5f6843fb7d0
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 0ef9dec8-7664-4619-b1c7-db5f2ea92262
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: df4a67ca-5922-44fc-b890-d9d785efe224
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: c5f20322-ef97-4463-b4de-5a67f5d29b40
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: b755b10b-9fcf-4171-9a0a-b984bd24e6be
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 94228ffa-0785-44a5-b6e8-9bbdcc40044f
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 63e709bb-cdcf-4e1c-b29a-dc404efccfca
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: 904013f1-8021-4928-bbc6-5d892d7c7e3f
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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: d929f4bb-6510-4b80-bc6a-22b9e1784d12
    creation_time: 2024-07-04T11:41:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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
