- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b59ec0ab-7a07-4896-9157-19bc9985d171
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a7a238a-fa7c-4b20-904b-330621e3379b
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 35
    column: 8
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86e8053e-bcf4-45c4-9d8b-5370ad94f1d7
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7c77ad7-bd21-4401-8b8a-4da4648ed844
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5e263bb-bc85-433d-bbf1-1e3ae650a0a8
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35581ddc-5a9a-4cfe-9f64-1ab418b45cd9
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96f6dbab-2a4f-4156-8175-a5abb67e66c5
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 628bccfe-5826-4fd5-8c2b-846d2f08f6c2
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1637aa40-691c-42d3-9eb8-2628d51b4468
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 40
    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: 82721e4e-7761-4a8f-b16d-efb1963db797
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4e6035f-c746-40d6-86aa-2f122040419b
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4747d0ec-d224-477a-9db2-b3bdfe9f788a
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e53352d-f158-42d3-b175-82579688d651
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 41
    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: f4adae86-47c1-42c8-8ce4-793cd9185707
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce8a50db-f4cb-4444-bdf3-69791db5ed19
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    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: ff4a7124-2fa4-4e6e-9568-80b15340663f
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1ef92ce-419e-4750-9f2c-6177c3e36bf9
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6917302-721f-4242-b848-ca2b693225c4
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 44
    column: 4
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f415db57-ac5b-4900-ae1d-dd44a58a3859
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e488054d-17cb-4f62-9000-e807ba958a41
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 30
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e679e411-02b2-4872-8662-bbf089a727b5
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d600cc5e-12b8-42f9-94d9-d37e88c00def
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b5861dd8-c2b7-4842-a5f4-51fe2a01e94d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce4c8702-83cc-44cd-a3e7-a1a1de52ecba
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0772f793-5d9c-4425-9591-d522f6f593ac
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 11e4aeb5-7dd1-44a7-9d0a-35ca1d9d00d4
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 708c9709-a988-4a75-9e6a-3212b6fb65c9
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_unwindbound2.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound2.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound2.c: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound2.c
    file_hash: 9fcd44eaa3ebd405f2b1e22097631bccfcd3fffe0471ba695e470043120f86ec
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
