- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6cc9ea2-d75e-4dd5-afc7-0f082a8ccc74
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46a37294-ad64-4cae-9a6b-8ca79709eccf
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02425d93-a0ce-4388-ad70-960b3f33028f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6859aee-976d-4a9f-896b-74fc25f943f0
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f9b4d5d-a8de-4caf-9149-1d7d868475da
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0513c14a-f643-4ca6-ad12-b64f9348b4d1
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89993a35-8ca1-460a-8f42-5cdae1d4141a
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2579553-08e8-4a09-8b8e-afbebcf0fd00
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c533d34-0bde-4d84-aa41-05cb34b0a4d3
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09d02c69-bb7d-4e14-8917-d8db6cfe435e
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088b677c-dc51-4623-bf7e-e5780993e951
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1da7f8b9-ea1f-4d0c-9bbe-53bc3c421408
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a753a0b-479f-4fd8-b1f7-2dbbd965c8b1
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || distance == 0.5'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 285c0474-f863-49f1-b878-7e14cde2cf4b
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd869957-ebaa-49cf-b776-527367fe0f25
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd6e6464-780b-4810-bf05-9b919d5c5847
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d717364-81ab-412c-84ef-076d112e2adb
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79eb6b5b-339a-44c6-bc2c-7cd09f28bc56
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c605560-7d22-4817-abd5-4e7ab41ea3da
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3305af4a-67e2-4305-a33a-69cdad2ed0a0
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e31b7b5b-4217-4767-a302-83a9e350b8c5
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19b06344-4bb6-43a0-87f6-f0870e2e8bef
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63ee500c-5c93-4965-8c3f-ffd52b4a8719
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4650957d-320b-491b-b52b-c86b06e29951
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfb2ed74-58b9-4c4d-b0f6-a028a2315900
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6461fe8e-f059-4b1e-bbde-3480a167ded2
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || four == 4.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a30f5e43-9486-436a-a647-b2fb9fdffb2a
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13372495-310f-4472-973a-be08081fc6e9
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00dbf9bc-21eb-46e4-b688-0f41df278b82
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c7943c2-cdb7-407f-a407-5a8adfe622e1
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d456492a-1ad0-4e88-b092-222ba4cff542
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 471ce8ac-a315-4804-8ef3-dcd2c1853767
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6828ef0-5a14-4de6-ab8a-77f255e08e8f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d19fa23-93b7-44f8-8170-0e3466089b21
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 103a1e61-0d05-43bd-bc4c-b35b8ff1d530
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 553521fe-d1fc-4817-81c4-58b2a98be6df
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9642456f-47a3-472d-aaf8-0422348af776
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4528999-b06e-4a25-aeeb-c7f192bcceec
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d9e3c85-b49d-4a69-a495-d2e79296b43f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || intervalMidPoint == 0.'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 926a671c-3be5-4722-9a1c-c74b5036bde8
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d9b50da-07d6-42ce-a714-5f572c9a8d70
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97870b92-4ff1-4d8e-b964-1f3768289eec
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3afc3b3e-e65a-4a72-a63a-80f5b98a5f9b
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dcf988aa-ad9d-498c-b53b-e61541a87222
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2306296e-31f4-437d-9b25-aca0fbda6cb4
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b57987f2-776c-4bbf-9487-986eabb81581
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff1d5d27-6d4d-41f1-b4cb-2e8dbeea470c
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24b37dfb-ceae-43ca-8747-f6be98a921df
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 403f40d6-acaa-4d70-b9d1-2261cd3cc1a6
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8139df64-ae26-4d25-9e43-7084ce7cc880
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f88c913a-410e-4d9d-be4d-bbd575e258e4
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d4ff478-815d-43cf-928c-cb18b432f31b
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= iCount'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9608049b-6d4e-48b9-bad1-6c2c345726ab
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a082a5f-99d8-4c5c-aa09-2fc401810134
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eed8abf6-ecdd-446c-93e8-907c12cbe0ef
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eaace200-6bd3-4cd4-98d3-d2da3e4bf582
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75fa98df-04fe-4eef-81c8-a607f973dcf6
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a0274c4-bc41-4463-974d-8c5b4bb65bc0
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20cf6e90-d7b2-4564-a0b5-446a6a165713
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83eae152-b5d4-4acb-956a-fbccd66b94a8
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e6d2b68-87d2-4420-9330-4e0ab70d4593
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d97cf816-eef0-4582-9bb8-8ea949b51d23
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79d214de-7bf6-45a5-8191-c9f07cd90615
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bffded1-6fc2-4968-ae8e-ae8d81e389f6
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfc84a71-6847-49d9-bfe0-e13bb7c5779e
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (1 <= num_threads && num_threads <= 8)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cec256f-d7bf-41b7-8e9d-65357dc6cbc6
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a551dac-d8fe-4d40-8d5b-a5ff6e99ec39
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b18d75a1-81f6-4005-a7b7-9785b1027840
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f25d657-8f56-4646-adc9-82f6dc7f353d
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ce4d315-d791-4f45-aa25-07cef8c4d394
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ee1391e-7e1f-4432-9fd3-42a3b74dcc5f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d0c8ebe-73f8-4e98-9507-0ec554738710
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a443cb8e-430e-4a3b-8991-8de4a45a1c92
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 540c4385-096c-4746-b213-c0ee33719cc6
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df3f6f14-9598-4cd6-851d-05e54a6690d3
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f80545b1-4c1b-48db-8fb7-737ddccc3d97
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1481837d-b8f9-45ce-a21b-85665009717e
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54b51dc7-e48c-4004-9ccf-9d8976a7bc8e
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || interval == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 289e185d-c5c1-4ea4-91fa-a5d242905de5
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42b7d1b0-9b99-4fd5-a4d2-ee43f03f1071
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7aa3bf1-1601-4c64-a6ba-9fa316cab5df
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4b4110c-8464-4dee-b71f-5e806fc1423c
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49a3b5cd-f47b-400f-8bc0-079c70f80561
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13c2ebef-f82b-4106-ba76-1af473f89c08
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 149be4c6-a784-4abc-b1d8-81872e177109
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e255a4c-4c6a-4e84-b4b9-9ec11d55d2c3
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c77b094-f756-4dcd-9bce-74c9966cc4ad
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b960470b-6d0b-49eb-bf9f-e9657067fded
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1f1ea28-8842-4cd7-8dc3-199f36af56ff
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26ffc455-87ad-459b-92f3-d1cab8aa3c59
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6bf74bb-367e-468d-af7a-7302c9c19c9f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || iteration == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4eb43315-3c5b-43c3-b506-0a29d0687afd
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f78290e-fb14-4289-a417-b55b3e3609d3
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1851a78e-55c3-4b15-b42d-136b10e271d1
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdafcd90-ea16-4d43-a6fe-5ccd3712333f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d9a7ee9-a649-41f9-975f-2f2c22e932c2
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 497e3d31-0cdf-4159-8bf0-1c6798c8d88c
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a21633d0-ab8a-46d5-8e0a-d0889d76ef7d
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e5e60ae-e534-4502-b19b-fef2871c422c
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5c42456-d9e9-4d5f-b819-dd9663c2c00f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6d0d844-377b-4222-afde-e81cb707f890
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2affc60d-d1fc-4383-a021-bd1829f1acc1
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c76d655-ba98-4a0a-a613-e982c085d995
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 690503b9-1148-4f6b-9bc3-3f1c49068f70
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || numberOfIntervals <= 8'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07cf01b9-b323-48bd-9912-4879abe05959
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35dce553-af3b-46a6-94d7-462351efcaa2
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0baafa97-7722-4536-9997-aa5500d25b79
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a0f3353-0ba6-4469-8fc1-19f7b985f2b5
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50d89e47-2261-4b27-99c5-6898b05f6e3e
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1f34125-eb37-46d3-b1ac-46584b5c7175
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3835d547-a8eb-46fc-b1cc-004b760a58bb
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 082a097a-1361-4d88-868d-24c18e4e1be2
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fda1db17-7bf7-402a-a599-df47c09b05c2
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9ef808a-c9cb-436c-8b1e-8fed819fb94f
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bbbcdf6-e9e6-44ad-b6e5-a0460e6f3221
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 710de296-a765-4cd6-bffd-7f3f5827a4a4
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1510490-e410-4af3-8b7f-32221ef01519
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1391
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || (area_mutex_locked || (((((((1 <= num_threads && numberOfIntervals
      <= 8) && num_threads <= 8) && intervalMidPoint == 0.) && interval == 0) && iteration
      == 0) && distance == 0.5) && four == 4.))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7565579d-a12b-44b4-a7aa-0bca8df61008
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: area_mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 51f1173e-ad81-4885-803c-111e53654076
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: area_mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1339
    column: 5
    function: myPartOfCalc
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 579adc13-12e2-49b5-bd8e-34eeceee54c0
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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: ac43a991-a605-4fc1-b696-2d0131fdb183
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      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-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1390
    column: 9
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bbce951d-6565-4d1b-8072-35c30e813f00
    creation_time: 2024-07-04T12:00:33Z
    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.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-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: area_mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
    file_hash: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
    line: 1341
    column: 5
    function: myPartOfCalc
