- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 181e9ee0-8469-43eb-9b7b-fd976b044819
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8dbba229-b41b-447a-b344-abd424e5904d
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da8d7c42-0201-41ed-b5d4-34c93fb08c40
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 003b2ba1-1991-4e13-ad42-b382d8532b49
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7b531fb-b78c-484a-893f-d25e917ea9d7
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd4fb1e-a853-4e92-9b5e-bc089cccded6
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb4caa33-d5a3-45d4-96d6-015f6b8afc2a
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7406c7d-e65b-45dd-815e-e46b6eb5e08d
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d068066c-b67c-4538-bec3-85740e4074f4
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cdfb00cf-b3fd-461a-84ee-c89211df7786
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca30620a-ef51-4280-a9aa-ebc32d9756bf
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adf50b4e-5965-4604-8a24-5119cac05ab5
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d923afe-00c6-4596-8919-4f9bfbe6e8b8
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i: f9c41a0459a4e53814ad7a68b11b59fdee53e177bc2b437adf5a829cee3cf120
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/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 || ((((((((((((((((((((-2LL + (long
      long )num_threads) + (long long )numberOfIntervals >= 0LL && (-1LL + (long long
      )interval) + (long long )numberOfIntervals >= 0LL) && (-1LL + (long long )interval)
      + (long long )num_threads >= 0LL) && (-1LL + (long long )iteration) + (long
      long )numberOfIntervals >= 0LL) && (-1LL + (long long )iteration) + (long long
      )num_threads >= 0LL) && (-1LL - (long long )interval) + (long long )numberOfIntervals
      >= 0LL) && (-1LL - (long long )interval) + (long long )num_threads >= 0LL) &&
      (-1LL - (long long )iteration) + (long long )numberOfIntervals >= 0LL) && (-1LL
      - (long long )iteration) + (long long )num_threads >= 0LL) && (0LL - (long long
      )num_threads) + (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval)
      - (long long )numberOfIntervals >= 0LL) && (8LL + (long long )interval) - (long
      long )num_threads >= 0LL) && (8LL + (long long )iteration) - (long long )numberOfIntervals
      >= 0LL) && (8LL + (long long )iteration) - (long long )num_threads >= 0LL) &&
      (8LL - (long long )interval) - (long long )numberOfIntervals >= 0LL) && (8LL
      - (long long )interval) - (long long )num_threads >= 0LL) && (8LL - (long long
      )iteration) - (long long )numberOfIntervals >= 0LL) && (8LL - (long long )iteration)
      - (long long )num_threads >= 0LL) && (16LL - (long long )num_threads) - (long
      long )numberOfIntervals >= 0LL) && (long long )num_threads - (long long )numberOfIntervals
      >= 0LL))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: d8b8cff1-426d-4e74-9abb-90a79e9407af
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-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: eec8757e-8297-4771-b3f8-2fc29bd9a457
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-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: 49aa81cc-b38d-4b1d-80f3-cf6d7f4748e9
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-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: d35a65d3-d8b5-44a9-ae4d-0e8246b89704
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-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: 03f6dcec-7896-4edb-875f-aa1288048889
    creation_time: 2024-07-04T14:06:12Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-C-DAC/pthread-numerical-integration.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-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
