- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28c8400d-b1bb-487b-9093-04b305287688
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a54805c3-686b-40c4-99fc-592a59fbacb9
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 719b585f-2286-45ba-b660-b58e0fd8321d
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 216cdcf7-07d2-4991-a130-2dda0e616b26
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 34
    column: 4
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d53f789-a0be-43c0-ac6c-1d517b543841
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a15e62ba-ff25-4803-8545-b3d141a94c23
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d27fd6b-bf21-4788-ac22-6fa140b3815d
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98b4d920-83ac-419c-b6cf-6f86b45d4f20
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 39
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcdb7579-9b23-4b64-ad5e-a3ff739cb2a1
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1d087c3-ab1f-4343-ab07-d7f3dd1c3211
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95b34822-c57c-451f-9874-1c9ef7d4caf7
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 730907a2-0f1e-4f2d-9893-2aac4adb50ca
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 056c9d40-9068-4533-90bc-7bc77b6a46fa
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 42
    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: eff8fce5-d65f-48c1-98e3-6135df47abd1
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 878c31f7-e347-4efa-accb-503a6d04769a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    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: 19f5bc49-7146-4599-8f18-3d8a822b261f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e46fbe53-b36e-4723-9b0a-30e3b5c5ef1a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 391f8be3-c828-4440-ab32-8dd0d3dd3fa8
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e97e1635-ef49-46c7-9b5f-d8be70d9119c
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    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: 2cd6986b-9420-4f57-9635-03bc57fee780
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ca28759-3851-404d-baeb-1edea96d6f7e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 44
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 104e2641-ba39-4b5c-bde5-621d1012647a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 44
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9328eaa1-7fdc-4374-bf46-99d3540b3280
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 44
    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: 0e870a8b-aff3-4a1e-8485-a40caef71ace
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 48
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3da17cda-5576-4902-aed3-abed3e206c42
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 48
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa28f11c-bae0-4b57-9b60-7190a20733f2
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 48
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea75cad7-13ce-41f7-af50-8ed36d4a02c9
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6dee1e50-0195-496f-a6c4-693e9b28142b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 50
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f99448c-f112-46f6-9fb1-69521a7703fd
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 51
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bff184c-7654-4b55-860f-ccc9f57d0d4a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 51
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44a499b9-359d-4236-bf8b-79ae2aaae1bf
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6e460f3-6042-4f6c-95a5-ff2a0adff520
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3440022e-3004-4819-8ff9-301661a04be8
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 95f13a25-6efb-4dbb-8947-2e481975711b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 30b2893d-4938-49a8-ba76-b703606153e8
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f9e07e9-548f-4c61-aa49-00414eec4038
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound2.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound2.c: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound2.c
    file_hash: 0477687fecbd3170f65e2eb11926275d6b3232cae024dd47071f89d509b612eb
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
