- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cb0aefd-b395-41b1-8e2a-3301519098d4
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 23
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84227d85-b521-44ec-9eba-167d2a360b7b
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 23
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db5b6d8c-2472-42b4-a212-59478af790f8
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 26
    column: 6
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7295af69-b994-4f76-b35d-739af23fbcb9
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (((-1LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: caf263e7-af02-46fc-a9c6-cdc9af2f8f6a
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 26
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa06f0bd-45ca-4fc1-b4e7-860d25f1759f
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04ecdea8-e97b-4014-863e-9fdbfa0db7e4
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 206bb417-a5e8-4fda-96b7-6f8c81b2e2b6
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 26
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c859c80-fdd7-4df3-9949-c3486b0bf7ea
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 27
    column: 5
    function: main
  location_invariant:
    string: (((-1LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 052fe20d-d9ef-4324-a3e9-3065d75bd330
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 27
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 672c776c-749f-4b6a-894c-9d16d9acd363
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 27
    column: 5
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a31abcf7-ba85-4573-ad70-fdc2381791f9
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 27
    column: 5
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10c2758b-a100-428b-bea4-927e68d5f875
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 27
    column: 5
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c40cab5-8f26-4fbc-92b7-41284267107a
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 28
    column: 11
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 554cd9ca-3e31-41ef-915a-4b923c03f924
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 28
    column: 11
    function: main
  location_invariant:
    string: (((-1LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcdd39f1-dee4-46f5-8d9f-bdff9860e941
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 28
    column: 11
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce372f19-7241-4747-a05c-2671718e8c78
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 28
    column: 11
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd4f535b-0438-470e-8cf9-24526b0b7d1d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 28
    column: 11
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf64f310-675e-465c-b859-70232645781f
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 28
    column: 11
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44fbb20a-3ea2-43b4-a8d9-e919234d1c2d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (((-1LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2da92071-25c9-48ff-9427-626532a7666d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d517635-52d9-415f-902b-820e796acffc
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 895c25c3-f2b4-487e-95e2-3e1f953d076b
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f3a1b77-f153-46ef-a5a8-ca7261fa35e1
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f35d3e71-f419-4ac5-881e-a0999bd73ca0
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (((-1LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c76bd816-3ae4-48f1-8498-ed3416ed1348
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 31
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb0a771f-8805-4b64-a6c5-86fac0c25c74
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2da57167-c3b7-458c-b1ae-ffdd9c10adf1
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e4c28d1-605d-4bcb-a4eb-d9c74d4a99b2
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1cfc0aa-a179-44b7-be4a-c426cf0fdc80
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94dcd406-9ce0-4711-a3ce-03cc41ed9dc8
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: ((-1LL + (long long )i) + (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b49a444-91a1-430b-bd62-466acb94b083
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (((0LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d99c208-5d50-4976-9bb3-877c3ef1c2bd
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7d035fc-9726-40db-8aa5-f6a1433dee07
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 352c2b12-3e7c-49ce-9109-283d4dd4ea2e
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a10f01d-c4da-426b-adc0-193fe69b476f
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6ecd196-16b9-4df9-9c34-ce43e4f0dd89
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 34
    column: 2
    function: main
  location_invariant:
    string: l <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd38b85-d1a9-4abb-9a56-28ff2209b13f
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 34
    column: 2
    function: main
  location_invariant:
    string: ((4294967295LL - (long long )i) - (long long )j) - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de28a1ea-5c7a-489c-9b0b-503b50982330
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 34
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 490ac0ab-3193-45d5-8583-009cf34029f6
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 34
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abd79eed-cda4-47ba-b888-40efd8370cce
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 34
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 700b4187-acd0-4f1d-b592-de390207d6ae
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 35
    column: 2
    function: main
  location_invariant:
    string: ((4294967295LL - (long long )i) - (long long )j) - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbb83703-7e73-45ab-8a78-ff6d0063f467
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 35
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4123fc79-30dc-4400-a685-31309519d6e0
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 35
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab10dbca-c0c7-49c8-9302-713e4f8d1b58
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 35
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 575c2c57-483c-4871-b63b-bb04d1d49222
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a206dfbf-9b79-496a-948e-bee96edc3248
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2ba9f00-22fa-4b7e-bce1-9e7876cf118c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e823c3b-8ae1-43b9-8fd4-9b9d9b081540
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 17
    column: 23
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce90c12f-8076-450a-b03c-2c3ed5c967c5
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    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: 1ceb6064-426e-43a1-ae44-c85ff6b17a45
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    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: cb2f1555-2ad1-43fd-90d0-7c5114f30e9f
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    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: 112eee2a-b3af-42c6-bf2d-588a90c5b51d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f10003cb-3813-44ae-b69a-f9dee10165de
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 17
    column: 23
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60af3c91-b218-464e-ba0f-13e069b5717c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    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: d250e3ac-5189-46f0-b882-e7398bb94d2d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    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: a8214777-339d-4cce-8a7d-29b2159df918
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    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: 354c5b86-cb8e-49b5-a8b8-8fe23f59775c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3594226-50e8-4a8a-8f94-4e31a427991c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c39fc923-8be4-4589-930d-af3d3602f021
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 356fb19d-2fb3-4fa3-a6ee-4474e4dc4c2f
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f670a3f-9351-4f62-9596-513a7999b5d0
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 285d5504-4c18-476c-8d04-1a29921cc7b4
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff464d58-ff0a-435f-a8f9-e63e4955945d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f5dc18c-9255-4adb-91ea-e15f76509a82
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06cc424d-52e2-4676-bf9a-f7877764a1b2
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf72edf4-c03a-4d89-b8b2-9ad379feb411
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f55017e8-9aa7-4b0a-9911-7b20acee1e92
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea1c91ba-28e4-44a5-bf04-a863447391ee
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 870e822a-9735-45e5-a293-59819d0ed965
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ffdaf80-e8a5-460c-9ea0-040e21e44198
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8f1c888-fbf5-4efd-8d40-27d77ed4cda6
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 191ab6f7-053f-405c-9257-8cb42b34784a
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e96e7204-9d2f-4f52-989f-c143a397ef60
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08d9453b-1c9c-4305-8d22-cbcb4dfdeba1
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d84b9c10-a1d7-41fd-9781-17310aaa1b20
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2319ecd-4f92-41e9-b682-9d9b1769b0d3
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f00a48c2-b203-441d-97ae-90ccba258e90
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6f74b06-b55d-41fd-8916-ba93037bc5bd
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7267c591-9756-47be-aea1-d7cae334e191
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b6fb030-707b-4e2f-95b0-f58bbfd98eb3
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 659f0973-3442-4613-bf41-dc15a3fb75a2
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee11ef69-2d94-43c8-9e90-b9ab017279be
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3ed45df-1087-4c17-a60a-90d7d9c44005
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76ff63d9-947b-4d64-ba54-1f5cba518264
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1967294-8361-4d94-b5b9-219aefd4bd85
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0dd0e7b-1088-4926-a5f2-9264ba9fa7df
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76e5f62a-ef9b-4d65-bcb7-df9f5845bf76
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bad4cb6-c4f2-497f-8bdb-24974bdf4292
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52b6e9d9-a2a3-4bd8-a627-41aa0d0baf97
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae6c1ff8-96ba-4c82-9c36-53263854494c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2d35908-07ee-42b9-8333-571979fb36a3
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28259830-1251-4e87-b951-643d958ee35c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3f1eee6-128b-4df1-8c7f-551fb9511217
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8564d12c-bed3-4cba-a0ce-824db5e9e650
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae91c721-4b65-4152-a5f7-c235e2922c72
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 822e6430-f080-4686-9150-dc172628e3bd
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d2ad359-e4e1-423c-b8f9-8024eef6cb58
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0882464-1434-4bab-abc9-300faaa9e00b
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e0af14d-b6e1-4b60-b8ee-af76cb34674b
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6dcdcc51-0775-4ff7-83e5-1478dc8d054d
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: l <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 88bd58a4-2882-47ad-9d81-b8752f17792e
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (((0LL - (long long )i) - (long long )j) - (long long )k) + (long long
      )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a460e83-3552-46e8-8923-d897c9d74bc9
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09e37a44-3c24-42f4-8c35-46648e0f1e4b
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 764aea90-9baf-4b5b-9794-89bb82821fc1
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6470eb60-c8c4-4ff7-ac84-64b2a3995a1c
    creation_time: 2023-01-27T16:31:07Z
    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/sumt3.c'''
    task:
      input_files:
      - ../plain/sumt3.c
      input_file_hashes:
        ../plain/sumt3.c: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt3.c
    file_hash: e30b5fab1e4d82c0eedde50f4c0c38801322108217030da03826d472d6d39908
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
