- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e3d3b7d-b8df-45d0-b626-1ed56bd200d3
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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 || (B_locked || (-999 <= g && -999 <= h))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96856d77-db17-4668-b221-2852871285b0
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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 || (A_locked || (-1016 <= h && -999 <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 742c38d1-4f9e-4678-88da-f27db887cd5f
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6ea8d68-c2c8-4092-ab72-6b712a07c5f9
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 877f7bc7-b31c-480f-8e98-9f8f88300a38
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e6e9bfc2-c9b9-4346-94cc-11c84dfc96fa
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 6bdb08a4-e100-4dd6-90a6-636251fdf405
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 195ca60c-917b-4620-bd50-d6b546b0daec
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: ab56d061-c5dc-4942-8667-0f4a47f3defe
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: b1fba1d7-69d5-4a46-bf05-feaa6af83fb4
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 65fbe925-f633-4712-8316-19f85178d916
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 2680ffdf-b620-4715-9f03-291e2e76f501
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 5a3206eb-ab44-4d88-8f6b-6e93085e83a6
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: a1d7c023-1999-47e8-8537-48b791160f41
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 269e7630-c5a3-4271-bbc2-45ec63158c4c
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: db7c1f35-117b-471d-8407-f7cb49d9f51a
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 37a2aa7b-4196-497c-a71e-9799a240f245
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 2418d287-4016-46b9-bcb5-7b7afa29c984
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 4170b8d0-2864-4cc4-a67c-e9bb0f5550f0
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: d68569b4-5169-4c46-a343-0b41acc54d45
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: f796434b-6f5d-44d5-b089-19d7f7507838
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 869c7519-689b-42fd-bf3b-b89e2f4b1b17
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 63303062-fa60-4840-8317-411597f8f850
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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: 186d012f-40f3-4ea7-92c9-11250193c73b
    creation_time: 2024-07-04T12:04:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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
