- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c89c978c-8640-40ea-8c1f-ccce9aae252e
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= sn
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb97f9ea-b72a-4762-8e67-ca3be5c30a45
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 25
    column: 4
    function: main
  location_invariant:
    string: sn <= 16
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 146ede9b-2515-4992-b480-97b48755c72d
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 25
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbc05893-c4fa-4376-8a5a-992dbf5650ed
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 8LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8131f51a-beaa-4a2c-822d-5eaa5b8ce44c
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: 0 <= sn
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e81666de-6543-4733-90d0-5049dd1cf81c
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: baf93cb7-34ea-4603-bded-f3b32474d36d
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: i <= 9
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d3f1547e-356e-45de-bcf7-68c33353f0ac
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: sn <= 16
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 564e32e9-0843-4a53-ad41-8dfc322d322c
    creation_time: 2023-01-27T16:31:07Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sum04-2.i'''
    task:
      input_files:
      - ../plain/sum04-2.i
      input_file_hashes:
        ../plain/sum04-2.i: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sum04-2.i
    file_hash: aaea6fef281249794f41087d72bdcfa92bd0b0609c0833888767b94608daa7f2
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: -1LL + (long long )i >= 0LL
    type: assertion
    format: C
