- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b3936b1-0b9e-41a2-959d-ea7a90b8939c
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      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_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1376
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= g && g <= 1) && (g == 0 || g == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8f3a2a2-e957-499c-929f-c2e277e9a9d0
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      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_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1378
    column: 5
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= g && g <= 1) && (g == 0 || g == 1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7c2763bb-aa4e-4886-974f-fa7832ca7e83
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8dff71bc-58a1-40e8-a814-b8faca2775a0
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1357
    column: 5
    function: f1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 87f1447f-0bb9-4792-aa77-ef4d1c0d4113
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1357
    column: 5
    function: f1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8a5fd455-7d3b-4ce6-9d0a-35f62ceb318e
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      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: d5998d37-2255-435c-8c2c-2ceb920f07fe
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      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_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1375
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c7523a36-e632-4040-a277-94abd14f120e
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1360
    column: 5
    function: f1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a69dc032-6db9-4e8f-a6ce-c8f24a955f6a
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1355
    column: 5
    function: f1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f181ec83-83e5-44cc-96c1-174ba4159d63
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1368
    column: 5
    function: f2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 890fb533-5ef3-4dbd-8b5d-229b93a100e5
    creation_time: 2024-04-30T09:39:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection-read'' ''--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_67-pthread_cond_wait_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mut_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_67-pthread_cond_wait_unknown_1_pos.i
    file_hash: 1cd82b96c01a730247618eab1464d47c03eec9013c1d245312913e94981f2bce
    line: 1364
    column: 5
    function: f2
