- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d9420cc-7699-4556-8987-f7048f3af2e5
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 6c919f0c-9a5b-4ada-bbee-897af111eb58
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f00a7ca9-b505-47a0-9359-d6ad6374dd48
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: fbf53bfe-4cae-4edc-b267-88e252dfe8b4
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 2e2aafaf-522c-416e-aad0-58c784272b10
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db3b8737-8e57-4234-8037-40bed6a276d4
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: f840f592-736a-41b8-bf62-99b6587af2c8
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: f5d99be8-63c2-4307-a5eb-b7004aa7fc2b
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 57dad6ad-b28a-42cb-9cb2-9742f4618202
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32975c37-4395-48b5-87ba-41f086f260f1
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 853a9897-aedc-4662-bf15-3e1c74e1a79c
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: b3a4e9b9-b220-4589-bc15-4f52c67a9ebc
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: f0655611-db50-4c59-bc62-f42054abb1b1
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: dad3f197-8fa1-4a91-b7bd-98ab4e2cd392
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9213648-2785-4372-b51a-13be057722a9
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: bc2c75e1-e988-49b2-a213-ee793f691c97
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 3c2d33b3-c8ef-48cb-a7e5-1c03ece09a48
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87ddb645-1854-4a60-b415-ba2f6ec94b8f
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 8296a7e9-c918-4326-82c6-0878ac9b1d80
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: fe8b0386-867c-495c-9742-39dcb1fa3551
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 112ad014-65cb-48fe-9ae1-c65fa10520f7
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: b8e34640-db51-415e-98ff-c6d187cf38dc
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: cb3ba5df-df53-494a-95de-3e13ac978fa8
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 89aeeea6-b807-408c-b77a-48926965df1f
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: counter <= 101
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2463e20c-2649-4273-9a87-b1dd1435553f
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    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: 0ea2db3f-b388-4aee-bea0-8ffd47b00f5b
    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_unwindbound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound100.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound100.c: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound100.c
    file_hash: b61db512cc77bff784b3cdbd5d852c5dc364bdc7776dcbb3369c7c75ae1fb315
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 100LL - (long long )counter >= 0LL
    type: assertion
    format: C
