- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 833791d9-9473-4831-8c8d-e4e894ebefc1
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 23
    column: 6
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4998dc11-30e2-4466-9ca0-eabb71bec512
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 23
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42d1b692-75ca-4c13-88eb-ec4aee21acd3
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 24
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b433fc2-060d-4697-ba0c-fa9bdeb5af8c
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 25
    column: 11
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a353a392-3c7b-4d74-8c0a-d1ed9588490a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 25
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38487eac-bca5-4151-9581-76b511e75750
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 26
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 676f8753-3d10-4184-ae8a-6b1602204cde
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 27
    column: 11
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c99398b8-ca62-4e0b-8339-accc5c671429
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 27
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0e46421-7825-499f-9d4f-31c30bd351f0
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 28
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdf2cbb0-264a-4026-82c8-aaa56e678804
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 29
    column: 11
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bcd990c-6a98-4079-b571-1be30183cbf2
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 29
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e441e1fd-dcf1-44e3-8e49-8a501662a0d3
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ce8996a-9f69-46bb-bddd-fa26fc29ee14
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 31
    column: 11
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dafa14d-0963-45cf-97b5-4f4f27ce6c30
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 31
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e6c8371-eb71-4bab-9484-1f302ee76b98
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00447781-2f47-4422-ad31-1b235e33f978
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 34
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b64c4807-8a3f-4867-b6eb-0e1d83022852
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 1U <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32626b27-7ff1-4c90-9367-5d004caaaff4
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 35
    column: 4
    function: main
  location_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d67e25b-b3fc-4c74-aad8-157c3a622925
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 35
    column: 4
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8f944ca-27c7-47de-9258-94aac1229c17
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )l) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6223933e-93cd-4198-9eb3-1c68f386b732
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 35
    column: 4
    function: main
  location_invariant:
    string: n != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb65991c-ae0f-43e4-b9a0-6220339e0151
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 37
    column: 2
    function: main
  location_invariant:
    string: l <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eaba98a5-293a-40eb-a6d3-c9b90171d356
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )l - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab3adaab-01d5-42cc-8a5c-ecc76387e760
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 38
    column: 2
    function: main
  location_invariant:
    string: (long long )l - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49a4eec4-7045-4a1f-a469-4cb4ffe3f16a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf91f124-e5b6-436b-bbac-e607877b1e5a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a55b19e5-52da-4e72-9ec4-e8ca1150576c
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a7ff9c6-efd8-4e98-a999-1ef523655885
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25b3820b-3a8a-453e-8391-97fd1f7472f6
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4abe2e08-eed6-4b0c-bcda-ea3c974ee888
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a35acf22-ccb5-429b-bcc9-d9cd2a6f4417
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 588ebce5-24bf-43bb-a198-d3d59f6dc6b9
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cebfbbaa-0929-4fdd-88f3-3ca6f786d062
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d27d727-a933-4dbe-95c3-a23c9b8fc67a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcbfb8c7-b457-4dd4-b096-761bf51ef880
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c69aac1b-2f74-4415-9057-23bcd9ce3302
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 971ae7c8-3f86-4498-9e78-9ca05055e784
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7729f3a-e196-4562-b2e9-a785aa23230c
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a39269f-af94-4e36-88a3-47d917a2027d
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0816ea56-6161-4066-903a-cbb9e3169d91
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d39e019-ae8f-43d9-8a8e-42012ec5057e
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abdbcdf9-6662-44a0-a1f8-4df0819211f1
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86903483-3fa6-4b73-86d8-596d180a6d0a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8444d9c-7cc8-4e13-add5-d307e12e5c0d
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b33834b-e259-4153-a473-37633ed7a692
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f13c1ec9-ca41-4722-a0f8-d76d2feab364
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 732cfa26-6854-4636-a305-b39868112530
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8998fb85-1b54-4a90-a2df-fe4149a3ec06
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0164f4ae-71cb-4bfe-ae28-4e07837da724
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d43a840-f4e1-44ce-b71f-10e7ec75115e
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 682375a9-94e4-4eb9-921c-25fb564efbcf
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbcb3301-ebad-4ba5-a159-842a269d87ad
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c40e36e-935c-40d6-9760-a22487459c59
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aac07127-d8a1-42f5-90f3-ad0df808a253
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 19
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f4b718c-e0bc-48b3-9946-9f180a7d4c90
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb5739e8-2502-4f81-8967-19445ee7a67f
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe9ab22a-eeb6-43db-8f8c-bc224c0f9bbb
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61fc1ef8-3388-4a28-aff0-6035c2954e56
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2146faec-5b37-47ef-9372-5b26aa451a8e
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9bd5a65-323d-4510-9001-f008772bbb1c
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d97cde1-3f53-4f61-9f00-cd9633152c68
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b37da9-ec1d-4198-a142-2779be67242e
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f4bfd02-8660-4edf-b547-3b0bb359a5f9
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05fc46d7-8f7b-42d5-9294-2a5c77a6b61b
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc164c57-1e9c-42e9-a74f-e5fb6a64e2fd
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4d9da51-9e17-4e24-8e79-dc1c0b6d4a07
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d74f82c-bdcf-4966-b8a7-6cb65eb451b3
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b03c4e5-a134-4c85-9079-dac48e36067a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 942a2b44-7f85-4941-bd76-c10b0ad16009
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db3f08ec-577e-41bd-a502-d7103f706c05
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59d9567b-4989-466f-a31f-8cfec610ab87
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a95389a-192e-4fbf-bd9e-e4abacf15173
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18bbb146-6116-4ab4-baff-f6e465d4de8c
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91fedb30-8924-44aa-a1e9-6f8e2c347b88
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e761272-baa6-4d20-8b14-b095ed67ab25
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c208039-5ea4-47e6-b9a7-63ad6d3b0e3d
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17dfeab7-776e-419e-85c2-656f2af93fce
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: 4294967295LL - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34fc1b3a-5208-4d14-87c1-9a76fd980a60
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8276420b-5de6-4ad3-bada-f08e8e2dfcdf
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67b7ebe9-7d61-458f-81ff-e5c2f3400c36
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cc84c02-ce90-4821-b3bd-7d36532014f3
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3fe23bc-6909-44b7-8b7d-30d56e746af5
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29d213b4-f818-4558-bf16-53516f57b69d
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e89f687-5d32-40e3-9751-fffb266f498a
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 17
    column: 31
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a65eacb4-ff66-46c5-bc46-56570725f816
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0156b2db-7192-440e-a192-1121ed4d6319
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e56e876-26f1-4efc-8175-f4d42ab94290
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29d262aa-7692-4a58-b92c-6f18a829f83c
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 15
    function: main
  location_invariant:
    string: (long long )v2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9f17a5d-241c-46cb-9cb9-b3ce13ec5dcf
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 15
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4914ba54-e6dc-4155-bb38-2375e02cf906
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 15
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5414589-dc0d-4f43-a8ff-4c8b3a975b3d
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fdfbe07-2443-4413-982f-1048e5312fe0
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 521832f4-bff1-4228-aaa4-21d4e4685220
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 21
    function: main
  location_invariant:
    string: (long long )v3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f620fe7-ca7b-4ff1-b98c-e5a29bc6ca45
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 21
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55c6af30-4fad-4f45-be76-1bc7e022159e
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f2ed4f0-1321-422f-be2d-33b43f486af7
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 18
    column: 27
    function: main
  location_invariant:
    string: (long long )v4 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 155dc17e-b3d7-47a7-a06e-1f6cec9af753
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 21
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a49375c8-05b0-4003-869a-37d659c99575
    creation_time: 2023-01-27T16:31:08Z
    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/sumt6.c'''
    task:
      input_files:
      - ../plain/sumt6.c
      input_file_hashes:
        ../plain/sumt6.c: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt6.c
    file_hash: de82799de2ea095f77ab5123d5095356e09513a5e3f99652881b2c8a322ca8c0
    line: 21
    column: 9
    function: main
  loop_invariant:
    string: l <= 20000001U
    type: assertion
    format: C
