- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e255d043-7e5a-4f5d-90f5-2eba675ff33e
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77b66165-2732-41ea-abe0-d9de6c4a60e0
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df78dc60-7e9a-4a0b-8e04-c7a99df7deba
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac6dac58-adfc-4c3a-94a3-38cf68aa3d9b
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70850002-d754-4e5e-b527-30f2f7791bcb
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd113379-755c-4225-9581-f3c8ed25ccfa
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f377a62-2c20-4fee-ad4e-558d1d9bd183
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3764327f-d75c-40d5-bce3-d24c082701be
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (-1LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6c08cbd-19fa-47cb-82a6-0b5cd16ff4b8
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16c3b72d-7eb7-4d45-8c4f-7efd282a06fc
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4165976-cac3-4b92-a80f-e0bc0f6428ef
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc20bd39-908d-45ce-a26a-8bdfe852ba2c
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38b1ae94-5eac-4861-9a0d-fab3bb9ff8fd
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adfc6fb4-e2cc-4d8b-bfdb-237f81ca24c3
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a32b5e1c-6e89-4ced-9cbc-32900fb6896c
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d3ed333-9a0c-4271-b2a5-e72e47f805f4
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc0d2324-8cb5-4da5-814b-b75afd05990a
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c269871-4ddd-4e31-82df-e2588826b06c
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f090319f-880b-4a5f-b542-7fb31521b779
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9be2a6b-166a-407e-bf89-d8e5ac93703a
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b8606d6-a915-465f-b9bd-07dde55cad0b
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 42830bd0-0897-48b9-8aa9-ec12b54b6136
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f014d40f-9eb0-4203-90f7-4079340a122a
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cdbb5fe4-8444-47dd-b95a-d7d39a824386
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo2-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound2.c: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound2.c
    file_hash: 2e05249da124fa8fd89a00721e51c7b41eff3d4952cff855bee564f7b5deef09
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
