- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 537559d8-2090-42a9-90ed-d2b4775353ec
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 701
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (C_locked || g == 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb67eb5c-7b9b-428e-85c1-06635e3748e1
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 701
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g == 0 || g == 5)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a045dfad-6fca-470e-b344-84b02cdc1f96
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 701
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (B_locked || (g == 0 || g == 5))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 924a3d22-70dd-4fc2-891f-226df37a5270
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 701
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || g == 0)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: be7cee73-7738-46dc-9954-8a59e2ef2cb9
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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: 7eee9ac6-56b5-456e-b406-9a4487ea0df2
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 690
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 25f676fd-d58d-4650-918f-c1c4c6ef5717
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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: f3dd3564-6203-4ca9-ad81-9478d8a7892b
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 695
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42915a7d-ba74-4230-a92a-cbb523116162
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 705
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 762eaf3f-0f2b-4467-b644-88267eed8c73
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 706
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 085d87b1-4d00-457b-bfa6-874eae70966e
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 707
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76fbc0aa-0893-4a4d-bb0f-ff730cbbdbdc
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 693
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5c36555c-043d-4e97-859e-ec320b786b95
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 688
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 81516a3e-bc6e-4e29-b2f3-a6f56f3c4019
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1379fa76-55be-4f97-902c-b88f1666f42c
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 702
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b707b1c2-8bf3-4b5a-bf6a-48bd1f8a994c
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 687
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5c5c76c4-a767-44f0-b99b-d14f8ce54eb3
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 691
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 748fb250-ba16-48b1-806d-17edfeeaf9f6
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 704
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9585cedd-85b6-49a0-8622-c07953e85122
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 701
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1cae3e7d-18e5-46f4-b79a-0ed70b0ea1a5
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 632c2ef0-47db-4acb-a9cb-2237795c68ce
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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: 73de990a-c022-4795-8b25-fe7fa981c833
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 700
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f623e7a3-e514-408a-ad48-4487377a02b0
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 710
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf9c6c3c-4da9-4639-b47b-db623c2654ea
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: C_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 694
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ccf65e1b-e708-4dea-9dff-91669da02ac2
    creation_time: 2024-07-04T12:00:40Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
      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/13-privatized_32-traces-mine-vs-oplus-vs-meet_true.i
    file_hash: a233f90faab2ceb8ddfb042463870c03c0794d3cd45b2ba20de731314559cb95
    line: 709
    column: 3
    function: main
