- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8548466-1dfa-4d5c-9654-baf6a3e2a150
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a0ad712-1604-4b8d-ade0-4b6947c57ea2
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 29
    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: 58114e05-fa3d-498f-8a65-9142f376c059
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f02de1e-15f7-45c6-8c6b-0f79d9de78b6
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 054eb169-2707-438d-b869-6f5c7a96abc8
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3842fe63-9aaf-4524-a918-5bb263b7b04b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 38
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3c27043-3d28-49a9-bd44-f7d228266d3f
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 38
    column: 12
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a60cc5c4-3932-401a-8300-a991ef502a75
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8849e3d0-f819-4713-9db8-ea46ede2759a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e31098fc-6696-450f-a6f5-21766c99fd57
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf146970-e1b8-4fc7-ade4-66da63b3ff4b
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (-1LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d1d5ba8-5ff8-45ba-9cee-691ebc3d57b4
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b255ddfa-d874-4fde-a61d-741c8cbc36cb
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    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: b0505daf-0603-474e-8a9f-c378f31f6b49
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b477088c-5eda-4590-b364-298d91c9aea3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ce8c253-389f-4c8d-aed0-05526fb81b35
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 289afb20-af18-4da0-99f9-136a481e86af
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    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: e00e85cc-5a83-4b5f-93a4-ef80179097fb
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7c07976-8f0f-4b15-93d9-1d780dc53e01
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    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: c5146e73-4977-46cc-84be-ed8e8ca6e18d
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    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: 525aef9a-de9e-41a8-ab53-fcfad0c26ee9
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    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: 62b894f3-c97b-4c24-aa1d-065934b949bb
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 45
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f52cbca-f9f3-47d4-b99d-82bfb551abfc
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 45
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d0597dd-e7f9-4399-9178-f76430acb8e2
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 45
    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: 564caab3-c77c-41c1-952e-d37bcc3de556
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 46
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e878ef53-7348-43fc-b9ad-a06b50b74630
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 46
    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: 6376f49f-928e-4234-9faf-a4e8c2b40b06
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a683c290-67ad-419f-a5c3-8f866524ede3
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 27
    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: 33ca5168-ad4e-4320-8b9e-e356b51241b1
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 95bd4cb0-94a6-4bf9-b7c0-17ff85bca331
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bf788c6-9521-4181-a686-6a46bb79765a
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3db10b6a-578e-4110-9fc7-44eb7e63cc39
    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_valuebound1.c'''
    task:
      input_files:
      - ../plain/geo2-ll_valuebound1.c
      input_file_hashes:
        ../plain/geo2-ll_valuebound1.c: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll_valuebound1.c
    file_hash: 15f2c27c8ff19b1764b20b7d08d4582e2b047f4871dbacc2fd506a74654d4ef0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
