- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 16a51ddb-4a23-44db-9877-337081523d5e
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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: 93467017-01cd-47ed-838d-7c5aaa24d8b1
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 690
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0e87f93b-7c6d-4d4e-a00b-fca50cd4e6ff
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 719
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8ae72cb8-87c6-46bb-9688-56a1495b7340
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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: 907ffd3d-3c03-461e-b580-cd8edb4108bf
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 711
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ece80159-eaa8-4e67-9a51-824d3e92c2c6
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 695
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 63d6331d-492f-4a98-bda6-5eff640e672a
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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: fa9830c5-e36c-4cf7-9d28-27ffaa61ae4d
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 706
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 16a37379-9438-486a-9244-289ca4a1186b
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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: 8ae54d69-ca20-4414-aeb4-36940120ca39
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 707
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a056d2e2-db4c-4f65-ac98-ad0655a138ce
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 715
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eb11c7ad-20f7-4c75-a26c-c39f728260eb
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 693
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9ebe063d-0214-4641-af50-c8ac5fe06438
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 700
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d733c9b8-9f01-4768-bc82-ab57fdbb6d7f
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 687
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 05084958-a6ff-4410-bf65-1ff91065acdd
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 689
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6e69592c-1300-4ae6-87ac-566080941fbd
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 701
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b844c95e-866a-4e26-82f4-2cb435de4762
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 721
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 17ce1449-e7bf-42ca-a3ba-052b8589b874
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 712
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aa7c7c5e-5916-4d43-a7b9-7be1952b4577
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 692
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 491e7f56-7631-48fd-ab01-3375f3b9b136
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 717
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c8bbfed1-6525-4499-a27a-6dccd02b1fdf
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 708
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72dd6e77-7b53-4fd2-b5e1-804fb498ff4c
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 718
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e80b5b3d-a6e3-4137-bd14-5d1bf07d41de
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 02680b01-8ff2-42c8-874d-feb86dfb321f
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 697
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0ba1421d-0cfe-4bb3-b5fc-d59567a7e82e
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 722
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4f52928c-435d-4839-8193-6706c3edc9bb
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 698
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 88013f86-176f-4a09-860f-3d3cb66bd71d
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 710
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b69bfb42-18ec-4410-9a2f-baabb336ad4f
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 714
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6ef27bf3-a32c-4a29-ac36-655f057594e6
    creation_time: 2024-07-04T14:06:18Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-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_24-multiple-protecting_true.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/13-privatized_24-multiple-protecting_true.i: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
      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_24-multiple-protecting_true.i
    file_hash: 5a41a1715a056c3cefb9e5b0430ae444adde5aa2f4e6078578085bf381d921cf
    line: 694
    column: 3
    function: t_fun
