- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4cbf076-a6e6-4d48-bb2c-f404aa664b3d
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= R
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8859b684-e789-49ab-9028-aa1797e011ae
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )R >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9ee5484-a4a1-4453-b00f-ded3ac8c3f11
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 32
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a93b169-bd4e-4ab8-b2db-e64ee7965937
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 32
    column: 4
    function: main
  location_invariant:
    string: u <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab0d11dc-fead-43b4-94e3-da462e952fe0
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 33
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4664e1dc-d59e-45fc-9ed0-38f6b369029f
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 33
    column: 4
    function: main
  location_invariant:
    string: u <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7371e26-4b97-4ac9-8d86-3e42a0b86a0a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45e6c87a-a5e6-4c29-9c4c-57996d2a4bd3
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a087dbfd-6aeb-4fc4-9bd9-d14553824ce4
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca79b645-6e17-4a9d-9b28-c4a3b9d0e3d8
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35afcf1d-8b5f-4ba7-9002-d17355ecf010
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 37
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0abc6ae-0ac8-4631-8102-93ff7a9f3cf1
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 37
    column: 12
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90f8c267-1fa8-4bc9-ab73-41e11d1f594e
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47f957db-8a6a-4ec5-8db4-c407f9e3cc7e
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 39
    column: 12
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b66191c-452a-499e-b246-d205c1689b8a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 39
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fff1499f-7864-4a03-8e52-f2de5659d899
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d3de413-856e-4910-895c-989cb63a82f4
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 1LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce4828fb-f65d-4a7d-8491-0682a24b6785
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85d76b04-9ea9-448e-976b-ff4de16b37f1
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: -1LL + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18d64a29-6443-4ca4-9a64-3c1208475cdd
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5f851d3-d430-4bac-846d-ee4000a3e599
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf39c407-7da9-4f4e-8b7b-3575a7debe67
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7456df2-47ac-4644-ab87-01f9d637c8a7
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05edbb48-68d0-4ed7-a56a-9f74af25c5f0
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a87efa49-62d6-49c7-9252-6eaa64e31260
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa57a020-1b75-4cb0-bfaa-15bc25a59e92
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49cf6627-71b6-43d7-9a26-2377c447049a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: (-1LL + r) + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07d74fc6-be32-4d1b-99d9-41e53170019c
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 41
    column: 12
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95b08b9d-3ccb-4271-bad9-b2da294d785c
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 607f490b-8b65-4acd-86d3-cf364c0b97a0
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 43
    column: 12
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6c605d7-e23d-4af2-94c6-12e45ab5f341
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb585980-2cd1-44ce-a188-630babb8a1bf
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 43
    column: 12
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54ccff49-4c10-4f72-beec-eb54ce012f2c
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 0LL - r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfdfb6f0-1efc-4717-a846-34fdaf79b9d9
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 43
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088993f4-185c-4e62-b8a7-6add88d8a51a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 44
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2edbd4b5-e11f-4ed9-9cdd-d37a38b344ac
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4df84cf4-e17a-4c86-898d-53a8ecb77ded
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 44
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41116709-ca0f-455a-9e53-f43d4dab1e45
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a896602c-8b32-4060-b825-52661e5c6a6a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (0LL - r) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9dc3653-1c82-4a5c-b2f8-aeea6f81690c
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 49
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33599716-14f9-4fc2-b5ec-2b95f3757829
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73e10d00-be12-41ad-82a8-32d53889687a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 49
    column: 4
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17056ccf-241e-48d2-8d6a-de97380c52ac
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b9f087-5d77-4976-a3b6-fb9c21f66e79
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da24b993-b55c-4f2f-88d1-6655d5cb1af8
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cf36c9c-f592-4ad1-92c3-ec248187a78a
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 0 <= A
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6e728d5-3ab7-4ded-9cf1-cc3325dfda9f
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bc21d255-c388-4c82-ba4b-666995ea5226
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ac8b1a32-cf7b-4924-b778-1207b889a37d
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f54229fe-4423-4403-a183-c9ecd457038c
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 15568d38-413b-47d8-82ad-0b2641e8cae1
    creation_time: 2023-01-27T16:29:30Z
    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/fermat2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound2.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound2.c: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound2.c
    file_hash: 40704d62e6828e524eeb24a4dc1771a4d2719fc47e6facdd014c5940cef1d5d0
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
