- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f86ed98d-ddee-4867-8160-2e8c163e8400
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 10be973e-8b0a-4638-a566-f5f27b4019b3
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 36
    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: 3256fa2b-53d7-4a5b-b89e-3f82d1d4cb9d
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 5d0c46f4-7c8b-4b76-90f6-525a571856d4
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 58916ccf-38e2-465c-9c03-1b1eac2f192c
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 38
    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: 942d9b44-ad09-4037-ad3b-4d8d4f19e1d5
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 30246bd3-dd10-4a80-a5fc-8c354ddebe86
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 2e261230-5e88-421b-a4c9-efb1de2f1fb4
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 2f07b28b-ca75-4218-97cc-59bc8be47057
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 18d7c540-e525-4b56-ab2f-8fb6c626044a
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: cd1fd0ae-b795-4549-8203-fc34bc6b21c0
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 029bc215-0b8a-49ab-910d-38c0518b1e50
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: e693376d-af75-4cfd-9043-067c78cd4900
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: e9dc6e64-79e9-4d77-aafc-c7a69ac47d7c
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 79c05f20-843d-4109-92c1-c85e23720f60
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: bce8d7f4-0fa8-4092-97e8-4061dbbebbf2
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: a0770e19-cdd9-48cf-a2f2-e2e652152f92
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 43
    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: 5ce4a0c8-78d3-46a7-8f07-17cb5a1665d8
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 47
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55769c0f-f2bf-4176-8178-65af2236912c
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e07b873-a7e4-4c77-8545-432d88ac17f2
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 33
    column: 4
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 915310d6-a585-4f63-8cb3-ccb787ef746d
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: e87fa970-a06d-413c-8313-a4b9a4ac899b
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c78dd2a1-8298-4fbc-8ada-11aa446e01a3
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: 182643bf-9316-45bd-96bc-d92380e4165b
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 61b56ec7-ef85-4b71-bcee-8733132a269f
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    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: fcec469e-8bf5-4b73-bf68-adcd68b52de8
    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/geo1-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound2.c: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound2.c
    file_hash: 7e2bf307cb8f7c9c94b988ac468881aa12e08b820a3a7e7ee2376cf91aff114e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
