- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bd2212f-661a-4e2b-8a1e-82e8fc32c423
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 728
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || -1016 <= h'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b183946-7668-433c-95cc-b154120e0ccd
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 729
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || -1016 <= h'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39407d77-dfd5-4bb9-9227-dd9eba8c60d1
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 730
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || -1016 <= h'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cfc97b9-a379-4318-a75e-be159779c6ba
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 728
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || ((-32768 <= g && -1016 <= h) && -999
      <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b75778a-3284-4d7c-8be7-86d79ade9834
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 729
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || ((-32768 <= g && -1016 <= h) && -999
      <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c38df4f-4033-4e2e-b431-875c7ca2505f
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 730
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || ((-32768 <= g && -1016 <= h) && -999
      <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8145101-0832-442e-b950-a65dd55f8369
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 728
    column: 3
    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: 65ddbd5a-35e8-46d3-8cfc-923485456403
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 729
    column: 3
    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: 6a68af66-5816-4b4b-ad95-b4164a8fd99d
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 730
    column: 3
    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: 7bc64f15-570f-4f8d-81a7-b4e8fcff046b
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 728
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (-32768 <= g && -999 <= g)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 513a4b13-9f0a-4f74-a90f-56339a0a9a47
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 729
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (-32768 <= g && -999 <= g)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f07b0c4-9ef9-447d-985e-b51b2eba26a0
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 730
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (-32768 <= g && -999 <= g)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 70771c4f-8bb9-4237-a9d4-e37062b475a2
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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: a6a927d7-bc93-4b0a-895d-c554b71f9b56
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 689
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42131017-f9d3-448e-8a3e-965642937831
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 733
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8ba3a099-7a7e-4547-93d0-91ca8bf87ff9
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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: 895c2e3a-0fe2-4cf6-beee-9fd53315b697
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 715
    column: 3
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e90a4f19-023e-4234-b952-480ea7541555
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 694
    column: 5
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 131d3bf7-56f5-4a9f-a2b3-dd5bb3d47a97
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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: 3b3f965e-b21a-4577-9e08-2ab1d8a0dc89
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 727
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e7700acf-e7e7-4b5d-86e3-c559515441d6
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 704
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bc65e8eb-1678-4291-a5b8-127b7e76efab
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 735
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 073b90d6-b914-4dac-8882-ac4b942223d2
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 690
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c0a99189-1d0f-42fa-9b6f-34bb3cef19b7
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 719
    column: 3
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e3cc4fae-bcdd-4e79-b5ca-55e86be7ea15
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 714
    column: 3
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a1da160-7d2a-4adb-bb92-48ee80f86ac0
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 736
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 60d73c2c-e4d0-4b30-a227-d95dafa08dec
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 730
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d8fcec1d-e35e-4e36-9452-6972c0c6c150
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 696
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 10668043-65c1-4a92-9aae-64ab9f91e916
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 718
    column: 3
    function: t3_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 51c401ce-1a07-48ac-9170-58f8d7f7f243
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 697
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cc47f47e-17d0-45ae-9001-985cc0951740
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 707
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 53835454-3407-4d77-8d90-a73131f3c282
    creation_time: 2024-06-18T15:02:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-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_21-traces-cluster-based_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_21-traces-cluster-based_true.i: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
      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_21-traces-cluster-based_true.i
    file_hash: cec155e54548239c459fec40910e358deb5fad2ceffa658bfdeefddd1bc9e166
    line: 693
    column: 5
    function: t_fun
