- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d00e0ac3-c61b-48d3-973f-97aca95f98da
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: e87f5646-2479-437e-bac5-efbc06433f8f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 365b0614-f149-4204-a024-12f0d082bacd
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 0c611f49-100e-47aa-b4b7-ec891d7be57f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 29f9e8a7-1701-4601-be51-e876b18a727f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 773273b1-8317-4316-8c1a-f0e59a641e3c
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 8c34f4b7-0bcc-4918-8b6e-3859f4c54557
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 87ee64de-11e4-40f9-af4d-8c08b9db2b6b
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 78640656-f92e-41b7-8720-78a5a2c64540
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 2ea5538a-4422-4725-83a2-f7317d354025
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: e94fd010-b415-4ea2-bec5-6a4271e1c3b5
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 348ee756-f98e-4a89-bac3-aebdc34f7b75
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 19bc2de3-586d-431a-94d1-bbb9747b8783
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 6ab2faa4-dfae-42f2-8035-f6ef1e0fad86
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 33cc7cba-7414-4f06-a6b1-1b463ef39122
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 7d392ae2-bc54-4ea8-a695-0a965382acfc
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: be576b89-d3e7-4f20-abce-059960cf56ad
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 4eea9eef-99b3-4273-9567-c7dcb774111b
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 0a647be7-cd11-4cd1-a2a6-f92f8a97e4df
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: fbe780b8-ab29-4a58-aa00-2795d8bc4e5f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: e72b02cc-109f-4fde-b316-0c322e518b63
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 9072229c-ed3f-459f-8c82-bf0107ec6009
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: d48afa11-51fa-481d-8a97-96cc915513d6
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 5a69e648-430c-47ff-a76a-6f2ddc42773b
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 7fcd3ebf-432a-46d9-9d03-08c2c508df10
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 1bac55a8-5c95-4fcd-a05c-45a43e1a16fb
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c4987acc-e856-4187-95a6-a97d6a8edd2a
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 3cbb561e-460a-4dd1-a0bb-4527e38e54b4
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: bff3cbba-24ae-498a-beb8-c1f84e0bdeac
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 163a6143-37f8-4208-baea-0527f50614bc
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 6a237024-7968-490c-a044-516cdcc41825
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: d53c48f6-bcf4-4e6f-b273-a1ef8a963fa2
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: ac6d314a-86ba-4c65-be6b-1696ad95f073
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: b4b55e41-0c51-4836-a7dd-a09c4d9b27b9
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: ad1d8b02-37d8-41a6-818f-1dad94046c8a
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 567ad8ba-7d8b-401a-803b-00d5af0e0106
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 30687121-8005-4801-a9d6-adc7826b6dd7
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: dfbdd3a9-259f-4e83-9463-9eeddd2fb9b5
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 625d5cbc-b33b-480b-9d42-00a44ea5d661
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: aa67876a-da0c-4fd6-a7c4-122b2cac70fa
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 32f3d5ff-5483-4217-9b21-dee28424b250
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: d2ad6a76-f340-4dd6-90c1-dc9317c5f4d4
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c4429519-2566-4197-8af3-a6f06044f624
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 1e450533-448e-4323-9c91-b5121134d351
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 676b59b7-69ad-47e1-bf90-dc968f9bd007
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 907fc5bc-9e5f-4a10-906a-2a765917a7b6
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: b7740dd4-7061-4219-9290-83f0d0ece38a
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: dbb891ff-2d70-428b-96c9-ee9e4448f4ee
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c8923b6a-6834-4da2-8688-0488d1d69e16
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 6382cdce-f840-4c38-b086-8ed6df5aed72
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 89b972d4-4566-437c-ae2e-c00cbd88078a
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 0afbef86-d448-4dd6-b6bf-3d0eef4e23aa
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 76641117-684e-44b2-9332-3e9fa748d0a5
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6cd06dc-ddf7-4191-9d21-17702a338769
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08349e02-d7c9-4297-a9f9-e9b399384823
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13829817-ec7a-46cc-ac89-1dcb152aa9e7
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82f2333a-58d2-49ec-83af-90f387d7c273
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abfedddf-6b51-4a96-af64-ccc0902a0d7a
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e662c96c-9281-4097-ab31-3d3877869496
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7389022-363b-457d-a766-fc1af3ed0241
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3eb86e0-2cdf-4322-835d-586ad944af0c
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cedc34e0-c7fe-4082-951a-3bd846a6cb9f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aae2640a-c77c-4a07-b018-10f69edf1632
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bd840c8-662c-4a9a-ad9e-8f170c159e36
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af47c7b2-40c1-420b-8db4-98075c70c8e0
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 <= num_threads && 1 <= num_threads) && num_threads
      <= 8) && num_threads != 0)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97ca7fb2-0f5a-4fa5-9f2f-253200357716
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 0fc30af7-d701-45ba-afb6-fcf772820bc1
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 43ffdaf4-3407-44cd-b477-8f6da212a8ba
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 7c9ed87c-4eb6-438b-ba2b-49dca83a0319
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 1495d8af-6ac2-434a-b598-69d31516aba2
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 476f0fe7-7d02-4f20-baa7-bd15a786169d
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: bcccc678-f75e-4cd5-b26c-b215096aea0c
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 42f3e407-8b09-497f-8af2-3c88fda2c512
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c9a31e52-c657-4713-b44d-17c0166f7bd4
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: e2921649-0505-4b08-b1ed-458c375e76df
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: be6067cf-d599-44bc-811e-5b5bf4d9a4f6
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 466d76ec-7e69-4491-bead-2748a7f287bd
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 1960eda9-a4c8-4625-8cae-5bbddf341dca
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 370cb738-28ec-49de-bd02-99ed944f29b8
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 41b15546-f2d4-43e8-a1f1-a0e4f551c52f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 7f69fa98-fdd8-4999-809d-6ed3025c49da
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: cb4ec9a6-de69-460c-af7d-57bec5e17091
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 60c31cbc-64d5-42b8-87eb-1bb0b69140b4
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: cfb01b1c-ebf6-4723-8197-05ababfe7df2
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: ee6d4278-d20e-4941-8e75-039e19084d69
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 124b8f8d-b65a-4656-a5df-1a8729ff4bd5
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 6a907654-3f94-4d54-8b1c-34e4914889f9
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 8e47cbb1-cd32-4d34-948c-916b244a5883
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 86f1a912-68e5-4cdf-af12-315ccb50c080
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 77c08503-d907-4adc-a5ed-8f082c55dc63
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c1a3074d-6017-4f70-8ac4-af246b556049
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c0d26bae-4868-4026-9654-c918e276ca03
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 1a24d517-6fe0-4b6f-bcbc-ebfde1154823
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: fcbcce3b-aca0-4e6c-a4b9-4eed4223b5d8
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 1f343495-dca0-4f35-9dff-ea9ebe2fbfbd
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: abeef7e3-9294-4f49-b84e-0b5d07985695
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: edae0647-5a62-4e91-a43f-32f3edae7640
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: c8d98d12-1200-4eff-9b64-9c1be611a2db
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 4d4b1fd9-f107-4955-b0fb-71d3e0354a65
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: cd14af18-25b4-4903-adbf-d1ac849fc3c3
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 31999e35-0d3c-4463-95ca-30352b406f22
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 84610afd-4e0f-4858-8a57-4473b960c350
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 26683293-f76e-4174-b5ae-2bac21a9b8f1
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 7d6436e2-486e-4d83-aace-ebdf46b26809
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 8c98f771-f7bf-4857-bdab-56533e9582b9
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c99624f-f14f-4253-a724-9f957d015042
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ab2d02d-2c33-4a8a-9c5b-47afd1c88fc0
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cd1adcc-bb6c-4c80-9c8e-415245f3f1f9
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 832a3d2b-7a32-4785-8d5c-0b7b943d51fd
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 083d2252-563e-452f-9d44-e060af2137ac
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c1ec6a8-bdab-4486-a6b6-91f92ff61c02
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b652ed73-a69e-43b8-97bb-80754fdf0ba0
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eba3ac5b-01e0-458a-9483-770315a88322
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c92839f7-c81c-463a-916a-9839b0eaf336
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c5ef877-73ab-4ec1-9248-1e59a3bde59d
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e295c975-34e2-449b-a201-95878275ea68
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a45437a-0f16-49e8-ace1-4a1c34935272
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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 || (((((((((0 <= num_threads &&
      1 <= num_threads) && numberOfIntervals <= 8) && num_threads <= 8) && intervalMidPoint
      == 0.) && interval == 0) && iteration == 0) && distance == 0.5) && four == 4.)
      && num_threads != 0))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 98b43ede-7e20-45f7-9f01-e66b8d490010
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 717156ad-5f19-4ee9-a28f-21e6c86ae60e
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 064db501-a36b-487a-9325-28a6fed586ad
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: 117418ac-b436-4798-8cb7-8b24f83f834f
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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: a5bb5dec-ebe1-4e2d-b0cb-9666312a32d4
    creation_time: 2024-06-18T14:59:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.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
