- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74dd3aea-2a86-4435-99f1-ef0b49e7e9a8
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6154b1a0-3f5f-4dac-bc22-70dcc3aef826
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 35
    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: 5f89179e-8524-4429-8321-66da8c9951ee
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: a449582b-dae7-4922-b630-833f8c710d87
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: fb4b918f-7201-4847-9fab-784ea95595c9
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 37
    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: acb75cbf-99ad-4c03-be58-e6c8b5580a9c
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 17726f5f-16d7-4b14-af2c-bbd1d559acec
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 9d8414e6-7cf3-465d-bcf2-583766cda3ab
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 491f34db-0911-408b-a927-725e6f4f85d1
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 40
    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: c014bb26-4fce-402c-b294-cc74c76381be
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db7e94ce-1160-4e18-9f00-51922c9ffb97
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 0ca7209c-e2e2-4bf8-968a-9d0ba1cdc35e
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 73f0dbbd-b1ce-4a11-a839-47e9ef69d0fc
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: f3758331-0a39-440e-aa9e-593b7ff27d54
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 47f53288-f91b-4c14-863a-94c5b3e370f6
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 7d1df45b-87bc-496e-a0fa-46713d220c91
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 4076187c-1842-49ea-ad69-46e2b5a9a8c8
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: fc096756-bdf7-4c9f-8b0e-9ec660f7c28d
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 50e3fa68-6dcf-4000-b7a4-27479f14989b
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 101c93c6-7f94-47d0-9d31-ab5b0da9cb50
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 5569596d-4401-4bbd-ae8d-e89001f86472
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 45759956-2f54-4072-b987-0def26e669d5
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 21
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 28386ad1-58fb-4f6f-afa3-dff20a14b914
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    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: 1fb9a59c-bb35-405b-b5f6-3e87fe079c5d
    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/geo2-ll_unwindbound20.c'''
    task:
      input_files:
      - ../plain/geo2-ll_unwindbound20.c
      input_file_hashes:
        ../plain/geo2-ll_unwindbound20.c: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_unwindbound20.c
    file_hash: 76a219f1c64e889b9539a62cf30988094d07e133bf7ccaa4e013534e44709a48
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 20LL - (long long )counter >= 0LL
    type: assertion
    format: C
