- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69cf4d81-e9d4-4c4f-8a87-ad4a304bf669
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 6ed09e73-9fd3-4d22-adb7-dde5cf2a4ddb
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f95ff42-4aef-4233-bbb3-7f2d7b93e7bb
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 0e7d9723-347f-4632-94be-bc1d82d0c1ba
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 38
    column: 12
    function: main
  location_invariant:
    string: c <= 2LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96a0cc5e-45a8-4b53-9b19-3321b3c5432f
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 38
    column: 12
    function: main
  location_invariant:
    string: c <= 127LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88d0d05c-9f76-489b-a573-09d68f623983
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 38
    column: 12
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75a45661-0da2-4f49-9ed1-85ed336a8169
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e831bbed-e431-4cb1-9f1d-35e9da87c80d
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 9664e0e6-121e-4953-b9e5-ad21ddaeb43d
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a186430c-7ce4-4c3c-9eba-ffc46b521f4b
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 3a2d4dd6-1311-4f40-b4fc-5e7bd2f130cf
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5fe2717-baa5-4fa6-8326-24dea354bbf9
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: a953d0e2-432a-4995-bdc4-7f44a1b0330f
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 47
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8afeb933-7caa-401b-8798-b1d398c8e496
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 49
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e28ac8be-985f-491e-9dd1-da63677ee197
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46de9dec-cbeb-446a-b895-176d6dc5059b
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a81b6b7a-ccc3-4c5f-9487-1a088cc1b255
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 16
    column: 8
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9873220b-0cca-4c5d-be8b-2ba05a8e600d
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 18
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b92bf594-3802-46a0-9861-5f8a9f071faf
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 20
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c273e46c-11d8-4e82-ba61-5851756075d6
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 991d28e4-06ad-4cf1-a852-5ffb3c2d65b2
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 11c53a07-f2ae-4546-89c8-4ae76709a73c
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: b09954c0-d510-4e21-8ff3-e7242b6fb185
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 57a9f396-b74c-4996-aad0-49a62cdcd169
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e00bc9ec-a79f-42ac-add0-b36dfa278636
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    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: 043aaa7c-0c44-417c-bce2-b2ebc8d64a0d
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2b4377f-e913-405a-a49c-c463c02414d8
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: c <= 2LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cce838d-91fe-425c-b979-c956540c8ebd
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: c <= 127LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 37b0b3cd-a51e-4202-9c61-3cd94d76a338
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 62b1f0de-e1f5-4942-a119-ac277051c5db
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 2LL - c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aadd7643-1da1-438b-8c09-f8f64514cdd0
    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_unwindbound1.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound1.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound1.c: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound1.c
    file_hash: bc74c1b33e1074c3a5a06ad6eff1da469d2065c9f566ce661be4cc84c215be29
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: c != 0LL
    type: assertion
    format: C
