- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: dfcfcc7d-9de8-47ca-98fe-2ea265ea14c2
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3b1b818d-cb97-4cab-83ab-3fbecc192cc4
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 690
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a619de0d-957c-4f53-9012-8ed01b9b7129
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 713
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c7a31ceb-897c-4d1f-b172-a43dbf27a6ef
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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: 9636df46-8683-4f68-82b9-686f39554f74
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 704
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f0799fdb-ff64-4912-9a2d-3da7b2958261
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 717
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 15f2bd1f-9ad4-4bfe-9518-16f01e8245d3
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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: 9d7dbca2-d374-4372-92d6-fbbcf648423a
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 727
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 70bf8a04-d4c7-490c-9785-b2161f5387fb
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 693
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 54469fbe-7e42-4f6d-b47f-5413b9fb1066
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 701
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1c77338a-0739-44a9-9545-19a8952371e6
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 687
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6d3db441-f3c9-4aef-9b71-944ebabde65e
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 726
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7debc85e-e073-49b2-a497-58609ed6718c
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 689
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a995af07-9faf-43ca-843f-ae78980b7897
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 723
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: af56c0c3-4451-4fbb-a6d2-4873dc7ab3b3
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 703
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4d47a7a3-7203-4dc2-858c-d676cc09c2e6
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 697
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e2dffc50-6903-4458-b380-94a9b178b75f
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 692
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c5e255fc-e54c-461f-a779-2bc5645d8da8
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 719
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 239f919a-856b-40d0-938b-3046adb7dd79
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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: cddb9d38-96eb-424b-b2d0-39ea2f82833b
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 710
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7f2f44c0-245a-47f4-b2c1-09d080ccf01e
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 700
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b30488ec-d62d-43cc-a9f4-2d676601df5c
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 720
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6f7d2efd-c679-49c9-8b2a-498bc39379b9
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bf5fb3cc-c89f-4d69-9fdb-4bead4cd2ae0
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 722
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: be651e4d-8af3-4cc5-b662-5e1ca2e542e0
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 715
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7e10d304-2024-4af3-bbf1-03b257b2644e
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 698
    column: 3
    function: t2_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2143726b-798b-42bc-9b34-44826eb8759b
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 724
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 772bb982-77b3-4ba6-839c-35f4ba983b36
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 712
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3eaf1958-f63b-42de-a542-aea7ce0667e4
    creation_time: 2024-06-18T17:01:57Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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_27-multiple-protecting2_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_27-multiple-protecting2_true.i: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
      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_27-multiple-protecting2_true.i
    file_hash: 2d0b9c4fc8b0005fb250fdf1ff8e25835b95e676b1936e4f5fe1cf72245ee5f5
    line: 716
    column: 3
    function: main
