- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: b8bf57a6-22c0-4355-ac6c-9aab8159a7bd
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ce90faec-8cd8-4c4d-9b65-4ca1db36ed84
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 694
    column: 2
    function: index_malloc
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c2ae004d-208f-47e2-8b70-e1ec3b512365
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      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: 7c073407-5d7f-4903-8357-5db620673c29
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      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/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 766
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 757e53ff-a238-4fc2-9a7e-e61cfef20f96
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 701
    column: 3
    function: index_malloc
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 99848af7-d8fa-41e5-b1ec-e42e31ad38b8
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m2_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ba0e7dd6-b27a-4d58-9133-1f04f888e8d1
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m2_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 757
    column: 3
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 26688ea6-f1e7-4bc4-ab7f-046c8679b49b
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 727
    column: 3
    function: push
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 904c7e24-a113-4f42-8b0f-d36c0040d8bb
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m2_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 750
    column: 2
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0d67ae18-2f0c-4cbd-8923-5c476f70435d
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 696
    column: 3
    function: index_malloc
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 94c2f752-542a-4421-acf3-d9a204c33b13
    creation_time: 2024-07-04T12:31:14Z
    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/pthread-ext/25_stack_longer-1-pthread.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/25_stack_longer-1-pthread.i
    file_hash: d8aeba05368f3114a9c95156cfeec5f871d57fefc291ffe35d850d07bff2e31c
    line: 721
    column: 3
    function: push
