- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ccd4db9-4e12-431f-8e62-8b3e1315587b
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 22
    column: 4
    function: main
  location_invariant:
    string: i <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38e76d9d-76c2-4231-a086-54069491bd2d
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1db888ea-517a-4814-9c09-be294f2b0fa0
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 22
    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: 5386c15f-4435-4b74-94b2-2eeb13433f94
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e54eea18-12fd-45ca-89fb-f22e09643838
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 22
    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: 8dba3c9f-4ff8-44a6-bd99-b5f11dec9e80
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 22
    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: af2285cb-9aa6-4c69-b81f-eae507a91c33
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 24
    column: 6
    function: main
  location_invariant:
    string: i <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb724231-799e-48bc-9165-86fa5fae6e75
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 24
    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: 53b67f59-7087-4131-afd3-1afbe1c45bb1
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 24
    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: fc86d299-de1c-475a-9cab-d94728255f0b
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 24
    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: 01db0098-e379-4911-aea7-57cf4e9a32ff
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 24
    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: 64055935-094f-43b7-93b1-83dcacca4499
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be67773b-9947-45ec-9c20-fb75b37b9835
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    column: 4
    function: main
  location_invariant:
    string: i <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37eb95b9-c4bc-454b-8582-5cf6b4b11400
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bffb629d-fab4-46d7-8522-b628e75d3876
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4900d60e-99cf-4a67-b1da-0f96b43d7260
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecc5cd9e-2af9-4a50-877d-2ff3c44363cf
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    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: d821ed39-a0ff-44aa-9c28-3997b92ceadf
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 26
    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: 190c31e3-e015-4eef-86fe-cdce80a9d628
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6eb6878-5b1d-43df-b497-d73964214066
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 28
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12878349-da7f-4cf1-a3a5-8e1e4bdb82f2
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 28
    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: 42513be5-e34f-4414-8940-273029aab8b3
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 28
    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: d2658910-cf1c-4f5c-aedc-7c2a2afa4d5e
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 28
    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: 1f371bf9-ba34-491b-a1c1-fa1cdcb422ef
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 28
    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: 19cb6dd4-d0ed-402c-b363-72d9b37fe780
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83248094-e61d-4a4d-a87e-d31b7f3559da
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: k <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94667315-2053-4bc8-bdb4-8f885acc84ab
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bb8bcd5-7b34-4138-8b61-7f0d056ba3f8
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79d5920d-0689-45b4-8bf7-55f495a91d0a
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )i) - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 516a6313-1831-45e5-b0b9-02e341a4dd04
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 30
    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: 19db7e82-268b-4799-b568-c54dc793271a
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    column: 2
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e907ded2-feff-4f74-ad8c-ac6ac9aeb671
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    column: 2
    function: main
  location_invariant:
    string: i <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a2b977b-4ac3-4b25-8460-7af6dd39310e
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    column: 2
    function: main
  location_invariant:
    string: k <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e119572-87d9-4e20-8f58-b1588b795163
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af2f6966-90c7-4018-97c7-83bdd30a1585
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28d53f25-3b51-4f48-887b-a3ab6d82d6c2
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    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: 672952aa-c19c-43db-b0a4-5eaee7fa96a1
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 32
    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: c68090f1-2731-45a8-9db3-8f0ee778fd74
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      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: 2a2ae15f-a7cb-47b8-a7ab-422765e5a2d6
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      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: a3e30465-171e-4523-ba7f-2f12ee5a7695
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 33
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7cd00c8-479a-4b63-b04a-ca0c09288ed8
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 33
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32603ea9-fbca-43a8-85a3-16a44237d487
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 33
    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: c3cadc44-2852-4c0c-814e-49586e0d6c59
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 33
    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: 1fcd863c-cb53-4f18-8988-ab9391c943f5
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 3e864f8f-b1ba-4f86-97ff-7c0037bc70c8
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 4e06f109-74cc-4178-acde-a1c9523a2e73
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: b46a8bc9-0852-4f14-a4c3-3d1fb84ce6cb
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: ff012fd5-21db-4f6c-a4a0-294f8b113be4
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: b30830b6-f20d-48ea-a9db-e11335c24ae3
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 8e83007b-7452-42e7-b676-964eed904268
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: f6d8efad-9d6d-43cd-b930-eaa2edd762cc
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 17968313-4e8b-4c84-92be-9687e7c9522b
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 6ad35864-6656-4873-94ac-68c60575f03f
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: b8960341-2a81-47e1-b16f-24b40e37cde4
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 45b1adee-d383-4ed2-b17a-b9896dab602a
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 6b69171e-35bb-4408-8974-cfeaad52c8b5
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: a06e420f-4dbc-4f1b-807c-0f9e8324db60
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 203793e5-9ed5-4319-a011-c99376e37db3
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 342d462c-f533-4be2-ac06-80b6377ae9e9
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 9c481c5a-8911-4b3f-b106-63faa4e609f2
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 616831a7-2500-4dea-854a-1a2a684ae4d5
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 48039d0f-0785-40ef-ae65-a5c361a7647a
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: e54b97ad-bccd-409c-b20b-53b963d9ebae
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 4a344b80-9de9-4c5e-b84b-3ee7163e78b6
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 364af476-57c7-4125-ac65-589815b7891c
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 319b4985-1ca0-4924-9c04-cbc7730e72cf
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    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: 7e5b1665-9dec-45b3-9699-cfdff86cf21d
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 20
    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: 8e443f48-5059-4f2a-9083-947ae9c98dc2
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 86b1edd9-ea6c-49b6-b1cd-962682362d17
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    column: 9
    function: main
  loop_invariant:
    string: i <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 14dc817b-297f-4974-b9a4-69fe82b8d000
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 01ffeb85-d305-429d-b35d-2a1d0a3fa007
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    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: 0285dcd2-c049-486d-be67-ba496c15c549
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d1d23085-629b-405d-9403-9290fb765273
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    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: e169f533-010d-4bcd-815b-accae66d7998
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 21
    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: eaf6e40c-4fd7-4f1b-b136-abb5e4d49d38
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a61be8a-3349-45ae-958e-d7f4b9209b9f
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c9c239a-1b8c-43af-9ed7-d07ad13886d9
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    column: 9
    function: main
  loop_invariant:
    string: i <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e63cc79-22c9-4f8a-bf5a-194b6027468a
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 508e4a20-238a-46a7-a1e5-2fd3ec5b2dbe
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f124b5a6-5462-4ee1-8cce-a301dee2f8fd
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e748759-2064-4874-b9f3-4007b9637de5
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    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: a237f2ee-34c4-400e-9891-73b29816adc1
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 25
    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: a92440d2-5c6d-450c-8283-460344e64a1b
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 48ac03ab-c567-44d0-9425-5b24569095d3
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41f4688e-8f57-4fed-b87e-366fcc9d4b85
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: i <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ab5f504-748c-44a9-a08a-0d85b378a016
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: k <= 2147483647U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d5ff616-a8d0-4afd-8eae-3b55ad61a458
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8781d23d-537e-418e-bf0c-957762ac4472
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b424a30f-4709-4767-b4b7-8656e36d4ece
    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/sum_by_3.c'''
    task:
      input_files:
      - ../plain/sum_by_3.c
      input_file_hashes:
        ../plain/sum_by_3.c: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum_by_3.c
    file_hash: cbdeb806056afbf44cc985ff91f53f00e848d18cfefb92d1f6744eb19cf6d91b
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
