- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90fcf824-2c21-43e3-8e33-b9d1af0b1cf5
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      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_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 698
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (mutex2_locked || (mutex1_locked || glob1 == 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 913794ed-df54-40e8-9f0f-8a43af8af43d
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      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_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 698
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= glob1 && glob1 <= 5) && glob1 <= 127) &&
      glob1 % 5 == 0) && (glob1 == 0 || glob1 == 5))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c6a14c49-929b-440d-8acc-3162e110e828
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a0fa4ab8-77ae-44c4-92a5-c6b4b6eaaff8
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 689
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 2e7ec4c6-6450-46ab-bdf1-a82f3831520d
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex1_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 11050a3d-a26a-4101-9150-7171b86f8bbd
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex1_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 692
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 074d8e88-4bfe-4ea4-ba7f-f7cf4b92b432
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4861079c-0b47-4506-95d0-854f1c9d3d37
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 688
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 58e5b27c-b37c-4d16-a428-804a3a83fac6
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      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: e109f246-312b-4021-80d6-23daff7c81ad
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      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_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 697
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4e210a4a-df29-4890-9917-30086108b074
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 691
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e358ba25-c657-4a51-a2fd-ef2d08b79129
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex1_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 685
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4d5272b9-5dbb-4417-9ed5-f723458d437f
    creation_time: 2024-04-29T11:03:21Z
    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_19-publish-precision_unknown_2_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex2_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_19-publish-precision_unknown_2_pos.i
    file_hash: 6dd4f5b1ff018649ffc6fcf6c400dcf6859c8fbe22bc4e1d68608a723e1e2f9d
    line: 698
    column: 3
    function: main
