- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05ae2e43-1d1d-4d14-9540-ef6038e0aa74
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 692
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (g == 0 || g == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5c8e4d6-1613-46ed-a178-461396e484f4
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 692
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || (g == 0 || g == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c15b7a93-3525-40eb-b178-cc4602e1ddd7
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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: 8d935c69-717e-4bb8-9452-ad1c971794d3
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 957b5364-352a-487d-a6f2-cabb090587f0
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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: 3f9518bf-2d9d-4115-b645-57b9fa7cc8bd
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 691
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c823e75b-78f1-480c-90de-3f2b8b859adb
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 692
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b0c52727-df85-472b-aba1-0f37e6f515b3
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 697
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9c9e3c9c-b235-4ddd-876d-8c757d37606f
    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_47-refine-protected2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_47-refine-protected2_true.i: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
      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_47-refine-protected2_true.i
    file_hash: f7e90d4b6ab0561c00fafe8b5db7dd972e67889e2cb8e9e72502cd51ce4f0a76
    line: 684
    column: 3
    function: t_fun
