- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ce128bd-24d3-4bc7-bb3b-846016af837a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 4bb71274-0cce-4a27-841e-3746ad610943
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 9b4b2cb4-8e7a-494f-932d-c5e3a64ba0fe
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 4cf936b0-da62-402d-b1bf-1b9e76d0f44f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 841481b1-95fd-424d-9710-cab54f67c8ec
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 14b17f05-7b7d-4c29-a61e-e454e123633b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 084658bb-c1a4-4205-a5d0-829b10596842
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: c4d7475e-0e4d-4114-b1a8-918e9dd88f7e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: b42826b9-c961-40a8-ab9c-79e7e93807a4
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 0103d018-b262-47b8-8f09-a87e084084ba
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 787c104e-9a58-44d6-9652-fab28043e0bc
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 39ce27b4-d552-49df-b8b6-019f3493db5b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: b8f2fc79-5226-43e0-96df-db557de4ae53
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: f88d6864-66c2-41a4-b53b-12114fdd3b9c
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: e6773d6c-0389-4fee-9188-7d31134ad839
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: a1b8c0a1-98cd-4f5e-bfc2-2c6c590f46f5
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 866bbe93-f78d-4988-abb8-3c16341e2ebc
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: ec02c5eb-8fcc-4ecb-8ea5-d564c75a0a77
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: ab338706-014a-4e85-84fa-b7767db4e2fb
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 617ccba1-57ca-4d21-bd03-3c8e254b2df3
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 4a9f10f1-29a0-422b-af0d-315791bdc7cd
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 3eb6aeed-5219-477e-96eb-c70b43706916
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 6dc36626-4111-4b56-b1ae-8f1eedcfd88f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: d4ae2a5c-55eb-45d6-a56f-a82823ba1a1b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 00053817-9a49-4cc4-933c-5c8c4995b319
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: dd7328c4-7f54-4f87-8fe0-475d1686585f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: e5abdd08-38de-4832-a1ec-cc906640b586
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 553947cd-ad3c-4c8a-a20b-56941fe63cff
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 56194159-5333-4cf2-89e6-e6d475ea2464
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 7ec3e4dd-af74-49e3-9a4f-a348ed5c101f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 9897cbbf-5c02-4556-a99d-854d62a7cb3c
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    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: 11b905bd-9dc8-4300-8e8d-85de710535e4
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound2.c: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound2.c
    file_hash: 49f2ec108c5a903d6fb66450b34a24ed5e1ae616285117448a3e267ae2f349bb
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
