- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa9816d3-e254-400c-9ca0-8b40cd078485
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 699
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (B_locked || (A_locked || g == 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7513b95b-6bbd-40f5-b951-a91f756015be
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 699
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= g && g <= 5) && g <= 127) && g % 5 == 0)
      && (g == 0 || g == 5))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c55f01f3-5dba-47ef-b12a-3e336d13e8db
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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: 1021d7df-e66e-4ffe-a6ad-20acbd5110e0
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 689
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5f11b6bc-e6eb-46f0-83a3-ebbd210f083e
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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: 5d25d6b4-25f7-42d3-a3d4-8bb1e2e04f8d
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 692
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76ae3c43-9952-495c-8f5c-96364e2c8d7f
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 712fe29d-001e-425e-b939-5626d9c33482
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 688
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c0d6f428-082b-43b6-8fc5-8226a2933868
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 702
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99559056-0cf7-433a-aac4-9092c9a9342a
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 703
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 38533630-16ce-4b8e-b6a4-09085b653d17
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 691
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f43ac4d2-5736-465d-bc12-81700239ca97
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 700
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2071786f-c638-4049-a728-aea82e877f0b
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 685
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 9f59531e-a150-446e-b296-adf3f78cda5b
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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: 9847befb-3fe9-4600-848f-027ce444691b
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 698
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1a6ec7f3-2012-49b8-a12a-219d913736fd
    creation_time: 2024-04-29T11:03:23Z
    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_30-traces-oplus-vs-meet_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_30-traces-oplus-vs-meet_true.i: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
      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_30-traces-oplus-vs-meet_true.i
    file_hash: 9f8eb81fe04afedf177636b6e0b2ff7ec90c549122dc143b3ac2872279b10356
    line: 699
    column: 3
    function: main
