- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad7ff6b8-4a73-4508-95c7-54c62551a0d5
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 1dc9bcc5-59ea-4942-8336-c6465f5ebc77
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: c74d3682-9c86-45aa-8188-5c9d96792239
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 8b583cbf-a600-4979-b6f8-971bdd66becb
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 0ebb71dc-8a6f-4412-93be-64d42840a3f7
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 1fa46e75-0c5d-479f-b573-570035fe23d6
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: bf9df4e9-74cd-41fc-a293-01bba121c4ae
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4083e2ba-33f6-4aa1-a5c3-6929dca8091d
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 86c76a59-c42b-4550-92d4-9318f8cdf92e
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: d8a1c301-e18d-48ad-a499-67a108142ad6
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 1277e2cc-73a0-4870-b613-f25ceb10ef84
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4d77f6c1-eee1-4777-9cd3-b16699a8bc0a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 379f2d88-f7de-432c-95ab-9346f35f7619
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 87fc45d0-1f69-4c64-9cbc-52245ae35b15
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 9d750129-6e6b-4bbb-bbbc-c353b1fad1c3
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 17ea149e-2c33-421c-8b9f-f27ec2a74500
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 387a8388-833f-4651-8de7-f78348f092c1
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 9222142e-ecc3-41ae-b982-e32075d33a48
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 0f8ebaee-d223-483b-b9bb-4869873c4910
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 05e1d0e2-c071-4f29-9ef4-fc6bb4201f89
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 31b729ba-568f-4ce8-af07-d35bc5d79187
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: d63ad6d7-5db5-4e09-8940-255e8a035f47
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 87770a02-6965-4201-9257-f1cb80a02f53
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: bb60af13-1af3-4954-8797-570976438f8e
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: cc44fee5-ad23-4558-b48f-766f152cc79c
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: e0852631-4f3c-4188-ab7d-357ba5f74278
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 23739bc8-e35c-4bd3-98f5-8151ca7aa7c5
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: ce019369-be15-422e-8c45-ad958815df4b
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: f869dbbd-63ce-43b4-9ceb-4821ccc401c9
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 3ae1829d-33d3-4b3a-a3d5-3bca1e944a86
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 966f0ac1-0570-430b-b4a2-20be43977b9e
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: ec53cc9c-dcb5-4030-8157-0fcd420d022d
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 0db3eaeb-d050-4cd5-8423-822d8085ab11
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 453df6e1-6af8-4871-8515-07f6c54dc4db
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 89ac34ff-83ce-4b14-abfb-25c7618cb65a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: ce0d5729-8fa6-4edf-b0c2-499cea678cbb
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 3c0c8fcf-be46-4b5e-9e83-a575471814bc
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a0114ec1-3729-4f7b-89d2-378e218a6d08
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: d72e9a7d-7100-4613-9816-fe56ac97f5cb
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 937b1df1-a0c4-459b-b556-4199e1cb078f
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 02bd6009-e007-4e2a-af59-0add19ba0fe8
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 41ca08a6-13c7-473a-9231-c79806e11689
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 810f03c0-e844-49ff-8c15-5637c6b27a74
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 306f968d-e29e-4c98-b35b-abb852bd4c33
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: b245efc4-9992-4ef0-9b86-0712dc4b2688
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 75783f8d-ffeb-48f2-909b-ea6ab8cd4e3c
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: e39cfd28-4c07-41d0-bea2-51ad437261d5
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 37f4830b-894f-4df7-b696-6cb878dfa7c2
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: be9a6857-472c-443f-a2bb-7c9d37e0a8ce
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4fa3b9a6-e096-41ac-b5f8-9cd80743aa1e
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: e1aee995-e6b3-4045-93f0-d38568d3306b
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4145d683-5847-4fca-8758-f6b7b5a46fa0
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 8e06d390-b0c4-4f5b-a37d-ce57a932c3cc
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: e4e4f303-ddc8-4604-999f-a52b5d1f21ed
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: e4312341-7d07-4ed8-a7a2-d7eb0d3ae66a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 57149b1a-3d4c-4aa3-8c67-9eb0d4e80490
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 0f970762-aed5-418f-b182-9eada8a1e3a4
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 1808f061-91dd-4852-adfb-98859c68178b
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 9894469b-8f22-407c-a647-3107f6ad136c
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 7967f531-2c20-4c31-b998-458fd685d32b
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 7b90b8a2-12ba-44f7-a375-a4a0aa1aa12c
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: d31996dc-fa4e-4c66-9e2d-203fd071ef3f
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 46d58ea3-ef4e-492b-b907-cc4538430f49
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 82ab709f-b8b4-47ab-bc0e-ac9aa4cb5969
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: fe6f89a0-710f-4fa3-892e-c8b0a4502de3
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 009ee2cf-e4fc-4dfc-a3ce-f71ea67f8941
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 1d40669a-cd04-4647-917a-58974a8dbe3a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a3c3094d-c86b-4373-8d7d-ed07d6c12875
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: f247cbb3-666c-46e7-b6ea-e7caa3345ac3
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a3ddaa05-3b93-470e-8d00-e6ac045aa310
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: bfd0ea2d-9ca9-49cd-a809-552f054e7cd0
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 937365a0-b09c-4db5-915a-a1a07912c1d2
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 645bc8ef-3ab5-4603-a4fb-24864aca868a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 1610624a-b358-4884-bdcf-37d2b5301c1f
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: c120807e-0080-4168-9375-18768fb3120d
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 5233625a-4fba-4bac-b169-5bb0a436cfe7
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a7ae6d98-b5e7-411a-ad6b-a1e9afd4c546
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 7c10822c-416a-4fef-9e2a-f54aa52e40b4
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 6d968bb0-2334-4464-a4b8-a21fd1e6a8bf
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 74d233ce-76ce-4146-9f9e-4061736c1879
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: c1fcd0d7-5b13-4486-af00-66117a7229a0
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: c0dd147b-cf0b-4133-a459-0fd36ea91d75
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 6e5b6c4d-5f0a-4855-a310-89d0e4b3ad82
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 31a24860-4b37-443d-833c-8f7d75bfcf2f
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4bc447cb-49e4-414a-91f3-6b376ed329f0
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 6fe059e2-d2b3-422f-a4ec-e6ad2df47c80
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 69ac6b08-4c8b-448b-a5c5-6e2fa59cec61
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: db4eac50-93fc-4887-be3a-ad3209e495b5
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 8f85d491-9cd6-402d-968a-ff96b5b72499
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 2619e2eb-c57c-44d6-9803-da4f0d763835
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4302cb11-3b16-4714-b1e8-24c166d83de7
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 06eddd3c-3c6d-4773-92d3-194e6659d8cd
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 575eabdc-7b77-4429-98a5-9a5e3418461a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 5abde52c-aeb6-4694-aca3-85631f61e38b
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: b6577209-d10b-47cd-a4d8-6592ffbe56e5
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 7d5de1e9-62c6-432d-85b9-e8fa71ad7cfd
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: ae15f336-d57e-424e-9b27-fdc1151924e7
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a5934818-3969-45d5-8c01-dcb278b63cc8
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a41cdfab-f1a7-4f74-93b6-2463ae7efbe9
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: dc9fc3db-59bc-4752-bd38-b61f593d88b8
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 19a51ca7-1def-45e3-bfd4-e50de6dbc534
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a2e71987-98f7-4ff5-a44a-eb0c20c12659
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 82ea60dd-5160-42b0-94a8-989d8d569ce3
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 70451a7b-0fc0-4a3d-8ede-032236f40f93
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 9585b8e3-ca95-4b2d-ac95-2de3d585493a
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: a941b4f6-70cf-40ba-8c32-22e33775793e
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: f115dc09-08e3-4fd6-abd6-d7c846937ce3
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 704a4bd9-bc98-4bca-bbbf-f4cd60044607
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: dcecd284-23ca-4db0-bf53-3c5b214fdc55
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 5a002b24-37c2-43f8-8dc5-e4b38c820920
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: d732695d-df74-462f-9903-4c39ee6a688e
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 58dfd55e-5fa3-4ff2-9045-b5c618fead6c
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 3726a679-aed3-44f0-8452-cee3f698ff9f
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 12cebf34-9cab-4c93-9065-315c4d4b4d44
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: b04c4a42-fc92-43be-ab01-ceeb893075b4
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 6edbe148-cbc0-495f-9fcc-efee9b6a06c7
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: c661ead5-a338-4519-8212-97103bc1b22c
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 5ba45c5e-e7b8-4021-bb36-7bc98c482ffc
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 12b718fb-e23e-4550-a06e-c8b1b3d229fe
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: d78cf09c-f189-41e3-9bef-e7f286802ba3
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 9a447bed-830c-4940-91c2-776d8e500aaa
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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: 4ea6111f-c18d-45cf-b5e9-edda2a95cfa7
    creation_time: 2024-04-29T11:54:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.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
