- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e50b86c-8c65-4898-ac7a-bb08c975a030
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 25
    column: 6
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d58e3c0-e4a5-464a-9a4c-69cad4ef56b8
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 25
    column: 6
    function: main
  location_invariant:
    string: ((-1LL - (long long )i) - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1addbd34-aa9d-439f-9bae-c06c7613d957
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 25
    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: 2d6bc0b5-2137-4489-a440-fc4f1b38cc72
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 25
    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: ae5588e1-4e06-42a9-873e-62de7ff6ed6b
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 25
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cfc8e19-e858-428e-86e5-365578199f29
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 26
    column: 5
    function: main
  location_invariant:
    string: ((-1LL - (long long )i) - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 655068a4-1e47-44f1-b2e4-d63a84adc319
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 26
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c1afcef-4a86-4f35-857a-fd83353ca85c
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 26
    column: 5
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35e9df20-3953-491f-acd7-9512c208899b
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 26
    column: 5
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d1383f4-b645-48df-bdec-07b57fd5919b
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 28
    column: 4
    function: main
  location_invariant:
    string: ((-1LL - (long long )i) - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7fc505f-ab90-404a-aa00-04441c6b0914
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 28
    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: f9bb1aa4-88f4-45a7-9f62-149faeac11a9
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 28
    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: e9819e40-350e-48eb-9e6a-b0b8b9c6963c
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6f66979-c499-4f81-8bf9-4695f0105e8d
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 29
    column: 4
    function: main
  location_invariant:
    string: l <= 20000000U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cec795f4-0a17-41bb-9e79-4f7af2cdd534
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )i) + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ff1ddfd-6189-4a9e-8ff5-a7af6cfe9feb
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 29
    column: 4
    function: main
  location_invariant:
    string: ((0LL - (long long )i) - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3976ac7-e4a9-49ec-b690-c78d781dc745
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7664879f-da61-488c-b86d-cbcee6c168c8
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52c39fe1-cc24-4777-8eaf-0b6ba0ec6316
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b925c602-30bd-4182-bc9b-2f98bb4f1b8c
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 31
    column: 2
    function: main
  location_invariant:
    string: l <= 20000001U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fa035be-7edb-46b5-bef7-1e76f924fc8d
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 31
    column: 2
    function: main
  location_invariant:
    string: (4294967295LL - (long long )i) - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a131ce76-9c6e-415c-8462-8dfd1113cb80
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 31
    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: 92a75259-205f-4b6f-a847-be6f3f748f21
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 31
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1c7c4ba-9995-4483-b745-124a27925f23
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (4294967295LL - (long long )i) - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2abfc2d0-8739-4265-a2c6-6b11a01cc62d
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 24de31ad-30dd-4cb6-a0a9-0cf28dfd59f0
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 32
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 527d445f-02bf-4d57-b674-8357641dffe4
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      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: 9d251464-1678-496d-982d-36e2daaacd57
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      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: 33e5a425-82b4-49e9-a48d-2a312e80de07
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2e460ab-94e9-4d2a-9249-a1fce5feb33d
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03496e2c-ef7f-486c-8e23-69f781bb162c
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44ced4d1-5c0d-4b57-ba28-fc1ea331d41b
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17229bb8-19b3-4fbd-8264-4c5586961fe5
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 918cafe9-4573-4ddf-b25d-36e46caa73fc
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 971ffeeb-7e3a-47bd-90c7-c632b5bc7c51
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffc68fbb-6c9a-421f-905b-5531e9bdcd13
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f11b60b6-794b-41d2-b898-8c66b1663e72
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 5ba9c785-d093-401d-91d1-90b28c190988
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 6041bb77-3813-4719-a747-e9ac3ff72cde
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51cadfba-0e64-44e4-b1d3-9d0f8cb6a574
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 55e1cc54-b4e7-490e-99c8-dbaeadc5eff2
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 8d9a961f-b60f-4e26-a190-030bdd103315
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ae272cd-786d-4b00-9ca2-47e23bbe38cd
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 4794231a-c37a-4741-9235-e0685727c271
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 8d143e4f-872e-4d3d-b996-49f9b3932b3c
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: befdcd39-491a-496f-95d6-2a0b895a78dd
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 9a3b0707-4e67-4c6b-8a0f-3d3cb19976c1
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: e80e4b33-14e2-40ed-a64e-9c8f416a2f4f
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 19
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83be08a7-b206-4fe2-bc49-feb82e61edc3
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: af0ec9bb-cc36-4a24-8f0a-64e374d79c35
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 033c3445-23a2-444b-ae5b-cc5222009f28
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 19
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 841d3006-b2b5-473b-8211-f62784f0f77b
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 027875a2-f116-4b3d-8dde-6a7aec4d63c6
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 8ba3d6c0-87b8-4241-8db6-29d58a5abd0e
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 19
    column: 20
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8de3bc8c-8183-47ef-81e7-e651a12593a0
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 82d88a00-96f7-49dc-b362-8005bef713b1
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: 3c33c530-854e-4eaa-89f9-cc50e426c9ff
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33641295-6b97-4d74-81c1-f26bc28f9145
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: da8a902d-8c57-40a0-b140-b3cc1fd5ab3b
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    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: e684e33b-56dd-45bc-bfd1-b6e1e48ab54e
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e1d4133-b0f3-4aaf-b68b-e7ea5cbed4d6
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cdce9e1-fb2c-4f5c-88f1-c321858088e6
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fce6a59-e57a-456a-8196-44d17dbd3660
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de7754da-5529-40d0-8b49-02e7ad40ce88
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11e92a9b-1249-4d74-ad42-8168cb0d772e
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 401fa485-0667-482a-873e-c41073dc6385
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c27326a-b338-44f8-9e12-74c949dff10d
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 23
    column: 9
    function: main
  loop_invariant:
    string: n <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f609e2cb-6138-478f-88f5-f9b1d5eaf084
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 23
    column: 9
    function: main
  loop_invariant:
    string: l <= 20000001U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c14a152a-3a02-47cd-b7a6-6dd058d45dc3
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 23
    column: 9
    function: main
  loop_invariant:
    string: ((0LL - (long long )i) - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fdeafc1b-04ac-4d92-9196-dc9a69d793e9
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 23
    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: b40d4e4a-3f08-473e-bce4-ff73270c271a
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 23
    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: d24b8e66-cf97-4b39-9f92-4e1d9b82e149
    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/sumt2.c'''
    task:
      input_files:
      - ../plain/sumt2.c
      input_file_hashes:
        ../plain/sumt2.c: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sumt2.c
    file_hash: 1b0e7d857a64a21fc5f03950cacb4a35900c867819a68273aa97f44e84e99e64
    line: 23
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
