- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 857e10b0-0610-435c-91ea-8ba51e58db46
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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 <= h && -1016 <= h)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47608936-317d-4767-a57a-20486c4bc4eb
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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 <= h && -1016 <= h)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a546a1ab-19a3-47cd-8ae8-2b8cf6e1e970
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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 <= h && -1016 <= h)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d87427a4-7846-48b4-977b-4246411a9f59
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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 && -32768 <= h) && -1016
      <= h) && -999 <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bdee4c1-c0d8-4700-9f11-2054f37d7b68
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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 && -32768 <= h) && -1016
      <= h) && -999 <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 539279cf-90f8-47e0-b75e-f765444d25e3
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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 && -32768 <= h) && -1016
      <= h) && -999 <= g))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5877e430-4c48-43f1-b9d9-33db1ea23b4f
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 15a9c97a-262e-4983-b601-7f031efd1108
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 453d949a-7940-4b59-a004-b066082671a8
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: da3c86c9-0ba5-44b8-a4b8-6dfa1804e927
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: f93425fb-f7c7-47b7-8903-be1991116180
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: fce6b8f4-9889-4b23-897b-848e7d4f438b
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 68436d8d-a861-43a5-88c6-6837467f9e0a
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: e095e4bd-c26c-4d42-830f-5a10f860f98e
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: db86899c-fd5e-41d8-a31c-c514aceb7681
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 48ba54cd-c51d-48f6-bf56-bf23480b3d74
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: b6f7ec1d-3301-4be1-b472-bdfd9926b5cc
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: e947057f-0f25-4606-9ec7-1cc017808da0
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: cfcb39b4-8823-409f-aa6e-48450e87916d
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: d99674d3-7e51-444f-ab01-1de0add6892c
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: aab76252-a04e-47be-83f9-691eb93c94a4
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 37cb54e0-fddf-46c7-a804-a8bf0ce7be79
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: e927faa2-5c92-44bc-84d5-107c49280f22
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: cb071e76-21fe-457b-814a-2f62decf6207
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 773f53f3-5378-4b6a-a16c-2809132f4f7a
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 14f89828-7bd8-419e-969d-3434aa1fe81c
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: e80319c8-fef8-4d88-bd9a-f3b3ec700652
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 0a6ad6c1-08ec-4f57-aff9-600c875cbda2
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 846b097f-93ff-484c-9341-747e78fd734b
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 006cfd12-76b5-40b1-8cbc-f07d2b695a2f
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 241b8934-10b7-4673-8ed3-a1d44c2036ce
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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: 474fba09-3039-45a3-b928-d096c04ceaf7
    creation_time: 2024-04-30T10:07:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_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
