- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7aad5528-e63a-46f6-98c5-96970459101d
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 695
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((g == 0 || g == 17) || g == 42)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00179029-3620-40dd-b93b-6da3c3907735
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 695
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (B_locked || ((g == 0 || g == 17) || g == 42))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 459cdbe9-e3c7-401c-8e1d-005a6ecadfec
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 695
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || ((g == 0 || g == 17) || g == 42))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: acc4dafd-0298-4b59-bfb9-44a67c35aa70
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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: da717976-e06f-48ac-8913-33ee99a27724
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 689
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 93757334-6a69-4096-9c8d-caeb66dc7e51
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 696
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c6cd86bb-413c-4f77-bcc1-7ff2f17acd98
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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: 3604497f-c799-4b91-a6a7-563466f58e75
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 694
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 242e0ab9-9f00-4d93-8231-b78d55d7e092
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 701
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f2d14e36-ff37-409b-a7db-e8f29de8a25b
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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: 71756ec4-ab93-4ff5-a9a5-d63c515b4d9c
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a5d2316-07e1-4dc5-aa80-de4e248ce2d6
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 688
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 90c824ca-435c-4224-8d39-902c70acf1b3
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 702
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 81292325-b7aa-4a2d-bc6d-13ee975109ea
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 685
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 87de065d-0052-4a3f-b61c-c3d874bfafd3
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 698
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6dea28be-c75c-4a52-ba1f-4516d778e7cb
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 699
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 18ddea27-db71-49e5-b715-e7fc9c5dc876
    creation_time: 2024-06-19T11:50:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gd3594c906-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_45-traces-per-global-and-current-lock-mine-incomparable_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
        : eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
      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_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    file_hash: eab672eda1edfc97284913525627300d4c299ae27e8726a3a4858e3cefa92c8f
    line: 695
    column: 3
    function: main
