- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1db9f86e-ab48-4585-a45f-6265c253ca2f
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73b0a5a7-8534-497e-8d81-2ae859f95f89
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2613656a-1194-45b6-a45c-49822a3fb39e
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5855366-0f0d-4db1-936b-4edb457f9bb5
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff10e698-c9ff-437f-b6de-f8678f4a5ae1
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ab58bcc-5bd0-4a5d-8e76-02768c9c60f5
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 38
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10406cb4-bbad-48f1-bf4a-22654a992d77
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 38
    column: 12
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6ee919e-46cb-4a90-8faa-9dc3e203e8d6
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a08efb99-4e35-433a-9747-f48fabdad383
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4dabf83-8a38-45ae-a939-4c1121a30b37
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1a0ee8d-a7b4-4a4f-8e70-216c1314d684
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 41
    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: 6a9a466e-60d4-4263-afbb-32d0385641bc
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9a5f5cb-c5a0-4a2c-853d-d8eda41bacd3
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    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: 6a8a6616-0026-4542-bfa3-142ad5dc7a81
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 925c4608-9e08-4e51-b6ba-83078d731b61
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0945935-a4bf-4be7-bc68-3110c9966702
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fec59aa-fcbe-48e7-981d-b7c0fcbdd708
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    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: eec49612-56f4-4c5c-b1ab-f6cf05cc08b0
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2aaf36c-ecc0-4762-9a70-3eff1fdccd7b
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6462c0f2-d89b-4547-bd47-1acf4eefea58
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 215cd713-e77e-45c2-b7d7-546adb261fc4
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 43
    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: 02027348-3c0e-487d-a914-e1587c45e34d
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 45
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d79c3786-4c2e-471e-87b8-f1b4560d08b9
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 45
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6ae59bc-8a37-4640-b293-cc5550127cd9
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 45
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 833abef6-aa19-47c9-868f-d58c451b6ea1
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 46
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57d85473-00c9-423c-bc93-1f4cd48dd0af
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 46
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0eda959-0097-4d0c-b150-b0cca0ebdddd
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cb09ba8-fe31-4c33-b05a-c54b119f3785
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c61258db-f22b-4bca-a9f7-24edbdbdce06
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea631315-9b1a-462b-80fb-752cb3a825cc
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fa3b5173-135a-4d4f-84f2-3396dec48a9e
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 97fdca60-bfd3-404c-bad8-1daa6e465698
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound5.c: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound5.c
    file_hash: aca349e1b3075e13240eff0eeaaa2d6c5037eeae5747b24322472cf3e2c19f6a
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
