- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bb13ce2-5b87-40a3-9e88-e7e083a6d7d5
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= next'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0db63355-7a39-4532-adca-4c89a761f5f5
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= next'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd28d682-b785-43dc-bc71-44391c509515
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= q'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21e5a32e-ee52-4b47-9382-2cb85c7c6dda
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= q'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 139be9cd-ac92-4e5a-b153-dd46ccdf5f33
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= x'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42c97a58-1a7d-450b-9063-717b36aeabbf
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= x'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f492d9f-194b-440b-a8be-5a7042912b76
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= p'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7aa636d-a29d-48c3-8969-93f0e539d5b2
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= p'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 703fde6f-9f6c-40a6-8f94-4bd79a1b4e1b
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= prev'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0580969-73b3-4615-a9a0-35e8651d2855
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= prev'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd08e8c8-0f07-4e09-9e39-ccbd437bd680
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= cur'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fe4403c-2502-4504-b4a3-6404e717400c
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= cur'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4757b66-c366-47c3-81e3-979c65bc6b38
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc9eaa4a-62e9-4e2f-9414-e2ff85e388fb
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= j'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11983da3-2d31-43bd-b321-995df1c74775
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 721
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= i'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64b686c2-059c-4cab-98c6-90586c153699
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 722
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 1 <= i'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 701e924f-2365-4acb-ae72-787c6f7a7b03
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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: f4c9b114-fe8b-4d5b-ade3-5c6be5f5385d
    creation_time: 2024-07-04T11:33:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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/fib_unsafe-10.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/fib_unsafe-10.i: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
      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/fib_unsafe-10.i
    file_hash: 89d9c43e2f37f1bac8114d01260f8a993f33530b50231d4afed1f3cf3859d385
    line: 720
    column: 3
    function: main
