- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3111aa1b-0eb5-4abc-9724-14afda549c9a
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: a56f4a79-ebb5-4ba7-8b24-3d702a547d10
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a98bc12a-33cb-4c51-8c83-b21911421854
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: e7ed217a-5584-40b6-a340-fbc0a31f42a4
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 956f8a54-fae9-42ef-abdc-c6275c4a4443
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ebff9d0-54a6-4c4b-9371-9764220b98d7
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 0d829757-ad24-43af-b78a-14c91c26b684
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: dbb5aaf5-0135-4806-a327-10f84cc9991d
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 15c6595b-dedb-477f-b1d6-c0d247b1c8b4
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bdf365a-3d81-4efc-a6ba-af040f75d746
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 08cc5cca-6dfd-4aa1-af34-c7b2783fa3db
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 6a5493bc-cdae-4187-9379-baf14becf0bc
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 4c471571-6d4d-41f9-9ed1-611db5682f2d
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 62104507-e975-424c-9485-e7103852fea0
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 790ba57f-1bde-4202-9b1f-d7457ae015ec
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 652460e0-d920-4554-aa1a-482f17fa5b52
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 5c062bd6-2003-420c-bedf-940657d23750
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa5df2c8-01b8-4970-b858-c35996e09cd0
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: b9728c3d-494a-4588-b494-5df41e2bb3d2
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 3bf385a2-ee20-4e6e-a4bf-361fcd98e0ec
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 888022be-4826-4c6e-b9d6-8d022e4c0cc1
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 17b88544-925d-4e96-b40e-e80e9387e5f2
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: bca6f118-d4d9-4964-a59a-bdee2a81e713
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 79971f23-cb3f-41be-88d3-19770d2c92c3
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: counter <= 21
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fde0b4d7-5b02-4c83-bace-319cccaff3bf
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    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: 22de90b1-0e64-42b1-990d-f8c9391735b9
    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_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo1-ll_unwindbound20.c: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_unwindbound20.c
    file_hash: 358d950fcb60363ca711e5ee684e998bf5a6b6b14c5043f9c788a7a76c08fd00
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
