- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 839df8ca-9625-4e6c-9fbe-bc55f8c503c7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: 0 <= left
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d0667c2-bf72-4ba7-b9f2-0182ceb367f2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9575ed79-a3d1-44bf-9d68-2f0068e5e51a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: space <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74e12ec4-8cdf-4919-921d-b00431b537e1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: left <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 629ce68f-8a01-4187-9ef4-1d0d7a37fcef
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea994304-783a-4f1a-b9bf-14d77ca55b43
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b6b54c8-24f7-49ff-89be-d43a426d47fa
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de59d84b-9694-4fcc-b225-f3dca0e8a882
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: (1LL + (long long )left) - (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f647ba21-a353-48cf-a2ff-3cc26243bc39
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 21
    column: 16
    function: upsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb299027-9d39-4788-b3f6-3272c4bc4e3e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: 0 <= left
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06c7f1cf-0f74-4463-bead-90fd6d8ff8d4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: 1 <= right
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 978d41b7-3069-4467-ae36-f779b7dad843
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: left <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c149f922-2bc7-4c83-8217-f9978d88ae34
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd6f8649-fda9-47fc-9cfe-c3d58dd8c2bb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d64c2c6-d499-4631-8bc0-03d930f2f443
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: (1LL + 2LL * (long long )left) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cd67182-b491-4baf-8591-57a2706a54b4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 22
    column: 12
    function: upsweep
  location_invariant:
    string: ((-1LL + (long long )left) + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fd85009-3f2c-46d5-8dce-88272a365ab1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: 0 <= left
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5340f763-b238-48b2-8eef-3d8d7864d8b1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af9de215-e08d-44f7-bf50-ba56b8e13d10
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: space <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 967c6f1a-13da-4027-99fd-e6d161077bc7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: left <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0e55151-01fc-4657-99cb-cc9584c0336f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 090b95f1-e5e5-4efe-9a61-22a7ffe68d45
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d44147f4-08ba-4279-a575-23538663f46d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: (1LL + 2LL * (long long )left) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1dfb1a77-6bbe-45e5-bbc9-313a7dc64bad
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: ((-1LL + (long long )left) + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9921fa01-9b8c-4507-a1df-51cede922674
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 23
    column: 12
    function: upsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f74de6b-5109-444e-bbd3-dded2dd9baa5
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 26
    column: 4
    function: upsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c9dd54f-9ae3-4bfe-8c92-53093c37d538
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 26
    column: 4
    function: upsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6347501b-4ac1-47c4-bcb4-6e338c58fdb0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 26
    column: 4
    function: upsweep
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4850453-f47f-4fa9-b0f8-f712ee872b38
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 26
    column: 4
    function: upsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a50b2334-dba8-415f-95bc-782b82136d8d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 31
    column: 4
    function: downsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e329899b-34d4-492c-8f98-73de405934a6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 31
    column: 4
    function: downsweep
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe59f5a1-75da-42c6-9d1c-d6dc579e0d9d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 32
    column: 4
    function: downsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3b03f82-83bb-4442-a6fc-059e923a9281
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 32
    column: 4
    function: downsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b47a0d48-500a-4886-bcbf-e4213bd22ffa
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 32
    column: 4
    function: downsweep
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10ac2361-f1c2-474b-8abe-b1e575be619b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 32
    column: 4
    function: downsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b059d1c0-a6af-434b-82ba-fa2b9b0b50f6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 34
    column: 12
    function: downsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf01c14c-7b92-4aee-a507-b20dc64c97e6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 34
    column: 12
    function: downsweep
  location_invariant:
    string: space <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca43cc48-f4d8-4399-8f08-2eda580da190
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 34
    column: 12
    function: downsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ee428e3-fa00-405c-8138-2a6e885e8743
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 34
    column: 12
    function: downsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f074908-6f8d-47f9-9948-029aad6c4673
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d105bc34-87cc-46b6-bdad-3b7040c55e03
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: 1 <= right
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51c52a3f-8ea5-4feb-933e-2313fb535f41
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: space <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3550ac5f-779b-4814-8898-68b35f501f63
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: right <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e97434a-c787-4b99-a9f0-de299b686ada
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 490b72ca-3433-4d7b-bcba-e58973fc9682
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99ef66f1-f80b-4e56-922d-3ff3bec00449
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: (1LL + (long long )right) - 2LL * (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00cd7a92-ac6b-417e-a941-c7dc4847b236
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b0562aa-40bd-473b-a596-57040570a0e1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 36
    column: 16
    function: downsweep
  location_invariant:
    string: right != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2085ce7e-4485-40fd-b77f-c9eaf0755ef0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: -1073741822 <= left
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b474e41-9244-4ca6-9cff-b115793daede
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: 1 <= right
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dee19a54-7aff-43bf-867d-351a6852e5e6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: right <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7588b3c0-7633-4099-bba6-47b96d043dc2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: left <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 530e3920-5b20-4b74-b4eb-8e893c1b2d8a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed862856-7cfd-46ba-b0d8-25faf5a70f68
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0789b67-4c56-4e0b-8a35-64391b324ecb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: (1LL + 2LL * (long long )left) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adfb2667-7c81-4aa6-994c-2a2b73aea1fb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 37
    column: 16
    function: downsweep
  location_invariant:
    string: right != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bce12cc-daa6-41b3-a6a7-3eb73cf62eb1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: -1073741822 <= left
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eab320f7-341f-442a-99b8-fa69ef8e6da4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: 1 <= right
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49c7c30c-4ff6-4549-b0f1-778df0fe3b1e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: right <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 660f185b-cbad-493c-aefc-c6b4c99b42e6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: left <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acafe33f-0be0-4c0f-ab4c-081daea1f2f9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15ad620a-7626-4e23-a0fa-b6bfb47c0d5a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d84e823-4546-4950-ac81-ee571543f4fe
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: (1LL + 2LL * (long long )left) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8abf990f-0f41-4665-a820-aeaef415a079
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 38
    column: 12
    function: downsweep
  location_invariant:
    string: right != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 662ba996-43c1-45ae-b627-1c2ee71fab58
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 39
    column: 12
    function: downsweep
  location_invariant:
    string: -1073741822 <= left
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b970ec6-5b6e-4569-9400-126417f90595
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 39
    column: 12
    function: downsweep
  location_invariant:
    string: left <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2e18316-2c65-4be9-b657-0a3fbfb6c0a9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 39
    column: 12
    function: downsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49c8f0e9-8709-44aa-b41d-65dc36adf965
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 39
    column: 12
    function: downsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f40d750a-b907-4b49-83fd-40b0707dc5b9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 39
    column: 12
    function: downsweep
  location_invariant:
    string: (1LL + 2LL * (long long )left) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42c61b98-0e90-4c60-9600-b9ff10add212
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1589f0c5-f656-49c1-b43f-886af1b782cd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: 1 <= right
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f08785c-a2ee-4be0-a0a7-767aaeb35f11
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: space <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1142c6ff-57aa-4449-8c26-1c980c874d19
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: right <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d62dbf80-0d37-452f-9009-f8f132a8d735
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: (-1LL - (long long )left) + (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82257710-1db6-477b-b3d9-b5fdf15653ea
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36e56cd6-09dd-424d-8236-ac99e7d8a169
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: (1LL + 2LL * (long long )left) - (long long )right >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06aa97f1-e45e-4428-8df7-682d57817786
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63af0052-34dd-4f4e-91fa-f80f672d4858
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 40
    column: 12
    function: downsweep
  location_invariant:
    string: right != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abd9c70c-cacf-46af-a975-0f0c5dc99572
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 48
    column: 9
    function: is_pow2
  location_invariant:
    string: 2U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 312780e5-e6c6-4fc8-b80a-78df7975c7ec
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 48
    column: 9
    function: is_pow2
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bfc2020-3407-4c7b-9e1d-6f6eea62c804
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 48
    column: 9
    function: is_pow2
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5573460f-dcc3-4fb1-a749-65b6276428b5
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 55
    column: 8
    function: check
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe71b957-4c86-4de1-848c-d594a51c7a68
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 55
    column: 8
    function: check
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87c8e148-07ab-46a1-9b5a-f9e106806880
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 55
    column: 8
    function: check
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14864945-e7fe-4533-b7d3-c7aaa8b7e592
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 55
    column: 8
    function: check
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a98db44-4436-4147-b3c0-7caefcce3664
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 56
    column: 8
    function: check
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04d2d8fa-05fe-4c6c-9e6a-b31605482554
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 56
    column: 8
    function: check
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6ae7738-58a5-4b3d-9dd3-2cdfa0e631ae
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 56
    column: 8
    function: check
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a645653-a696-409d-9f46-7feff302e1fd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 56
    column: 8
    function: check
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d4220a6-92b1-4103-9f7d-baaab7c27b79
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 58
    column: 0
    function: check
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9da7b80e-6d10-4019-9ef2-760a4d3d8495
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 58
    column: 0
    function: check
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 138fef48-cce2-4ab8-af61-a5afaadf8a01
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 63
    column: 4
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84d7110c-ae9c-419c-a44f-631f92174eba
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 63
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bc65d37-fbfd-481b-a0e5-7ac678494e09
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 70
    column: 8
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb7661dd-6b01-4aff-bc00-90924dff6c74
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 70
    column: 8
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f583f084-291f-42ce-b965-79b72572a04a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 70
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8811c0e9-ebee-446c-b32d-8dd2ee4544b1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 70
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9067fcf7-94ed-4eab-a936-96bc66ede8fe
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 72
    column: 8
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75b026b9-2fb7-4c3f-be81-c965f0493f40
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 72
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e91ef45e-6cf4-49c9-8841-7d07d97da876
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 73
    column: 4
    function: main
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 714b5f61-0913-4fe9-b9e8-bbb8b8520ac7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 73
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f01bf403-f100-479a-a01b-96dcb2b64fbb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 73
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abd980d5-dda2-4198-b44d-941cd86c58f0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 73
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0881aac-1599-4c85-93e4-50b6c8ad0821
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 73
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07c5e198-ab24-4ec4-8d14-3209fa12a7f9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 73
    column: 4
    function: main
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4b6f8b9-8af5-423f-a66d-845a8f7c7b4d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 74
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9efae0f6-747e-4733-b86f-8ca20e2e5f03
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 74
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dd8a3db-07e3-4978-ba1e-8e6f0adc3164
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 74
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e422928b-6e6e-4f94-ab14-394db48110d7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 74
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7a01b7f-b8d1-40cc-ab96-62f1d49af008
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 76
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05407f51-31d6-4b65-a6ed-a1d8edafb070
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 76
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1245e862-c00b-48ae-bc73-b1e825d76756
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 76
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d69ad9e-ebe1-4c80-9890-14102243e6c9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 76
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0add6472-b646-485d-9e55-777df6fabafa
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 77
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbecd99e-382b-4e17-8253-bf53dde651d5
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 77
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 179cd25e-4c40-4b41-aecd-03ce9075a3ce
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 77
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0bf3dbd-ca74-457d-929e-5ab77c1e4f3b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 77
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c6be4ff-b966-4891-802f-985782df2f29
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 78
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 052f042c-7190-4703-a70a-70f89af03386
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 78
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )n) + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: daec55a6-4bd3-41f3-b3ca-7fa609f982cd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 78
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 839bec6a-a5ab-4a77-b9cf-8dfa275a52e6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 78
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55158c5b-cda8-49d4-a139-e203bbb37901
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 19
    column: 12
    function: upsweep
  location_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5130c36-8049-4f6d-823e-2669c4312ed3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 19
    column: 12
    function: upsweep
  location_invariant:
    string: space <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92a416c4-56c6-488b-b04a-7b9e51db474c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 19
    column: 12
    function: upsweep
  location_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4206207b-e54a-4f7e-86c6-076e006ba995
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 19
    column: 12
    function: upsweep
  location_invariant:
    string: (-1LL + (long long )n) - (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a73dc73-2581-4dbc-a49e-9240a866e6de
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 19
    column: 12
    function: upsweep
  location_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8369bec6-e72c-4fc0-a872-af466003a5f6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: 0 <= left
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 15a66914-e000-4acf-ac6b-0380b6004cf6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa6c5d98-cd72-4ac7-afaf-e1cbc0059bed
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: 2 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 440283d1-15a7-42d4-b060-3686e56bc1d7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: space <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2439f9f8-51f3-4f65-a2b0-ca33d000fccd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4331aea1-1888-45de-97f4-0eaac6ec9c8e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: ((-1LL - (long long )left) + (long long )n) + 2LL * (long long )space
      >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2df491da-3667-418a-9121-0fd22d63ab61
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: (-1LL + (long long )n) - (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 610a8a36-26b3-4280-ac1e-27363035a589
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: (1LL + (long long )left) - (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e39a336a-c323-4d2b-ba18-ee4a01bd120d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f0f30cb0-e7cd-4d4e-b8dc-ae3861a12d7b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 20
    column: 15
    function: upsweep
  loop_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f84abaa1-5e7a-4ea6-b4f0-85bd583115af
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 33
    column: 8
    function: downsweep
  loop_invariant:
    string: 0 <= space
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c371514-19db-4075-9e8b-3736551263bd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 33
    column: 8
    function: downsweep
  loop_invariant:
    string: space <= 1073741823
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b034fc2e-d492-47b3-8da2-6a16d80f2624
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 33
    column: 8
    function: downsweep
  loop_invariant:
    string: (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bced9fe-d7fc-4506-a2d6-9440df2cc61d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 35
    column: 15
    function: downsweep
  loop_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 008c02ab-b0da-4d36-8d24-5ac8fd5919d9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 35
    column: 15
    function: downsweep
  loop_invariant:
    string: 1 <= right
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e46a2ef-4500-4624-9098-9873acaf232f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 35
    column: 15
    function: downsweep
  loop_invariant:
    string: space <= 1073741823
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 78acdbb3-6342-4d76-8553-8952b77257e7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 35
    column: 15
    function: downsweep
  loop_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 50a39846-6e7c-4896-913a-ea4cb99ae7b6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 35
    column: 15
    function: downsweep
  loop_invariant:
    string: (1LL + (long long )right) - 2LL * (long long )space >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7c7f4df-5aaf-43c4-83f2-b9e5d29fd361
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 35
    column: 15
    function: downsweep
  loop_invariant:
    string: space != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 24bfb3af-91fd-4534-b0f0-ea65d75159ec
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 54
    column: 7
    function: check
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9112fa6-73d0-4cfd-a68c-897085fbef78
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 54
    column: 7
    function: check
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c2455f4-a41c-47ab-8a36-86dbf0c9815b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 69
    column: 7
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a660d8c-c5b6-472d-abef-79b5a89bb274
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 69
    column: 7
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f1cc075-772b-4bfb-a510-e79912fa87dd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 18
    column: 8
    function: upsweep
  loop_invariant:
    string: 1 <= space
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 368568bb-9ff1-47f6-a630-4405d2e6bbf0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prefixsum_iter.c'''
    task:
      input_files:
      - ../plain/prefixsum_iter.c
      input_file_hashes:
        ../plain/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prefixsum_iter.c
    file_hash: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
    line: 18
    column: 8
    function: upsweep
  loop_invariant:
    string: -1LL + (long long )space >= 0LL
    type: assertion
    format: C
