- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12b3f834-db35-462d-9065-18497ea7dfa3
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: bbc59f28-5c84-4912-aba1-78161a060b0b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: c2c4a8de-c2d8-457d-a95f-f0a025894661
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: a7b21bf4-6e8f-455e-9b6b-a674aec0a0bb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: e0ec6def-4bf3-4c21-bff7-358c88dc3575
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 1b014030-3728-450b-a40b-be82a77f44c6
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 37aba171-fdc9-48af-b818-2af670f7cad8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 47eec3bf-054c-46f5-a73a-e36bc533d60c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 869ba889-3b14-4775-a05a-fc367b49dbcd
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: a084e58a-c27e-4be2-9a44-84d1e5e27d57
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 6741f93d-3159-4075-93a2-b2791964e112
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 3f28254a-dc75-4255-959c-406a8965604b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: ea8b505b-0726-4378-949e-42bf3230077c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 8c9d4d1b-b19c-4028-9065-3ca3606cc026
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 95bf1a7c-0a38-47dc-82a6-bae308bdd736
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: ccba7889-d0d8-46c8-aab9-b46acd600f5b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 8a580f99-7821-4f56-b53c-17074a32b9df
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 1cbee1a4-25ef-41fd-9af4-9f530d383a62
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: b2393f96-919c-4941-9b42-09f06376913f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 95171726-d961-4e80-a10b-994de085652e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 74abf934-8299-466b-b14f-bcac8c9d6160
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 3a780701-ecd1-4405-8a73-8b45d31852e0
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 4a8334e5-3485-45f8-a414-62b9c57c7995
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: a46b655e-c507-4016-86c4-31ba27d05889
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: d1ff57cd-eadb-4fb6-b9f6-d8e2a275b78a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 19ff490c-224f-4e03-a180-1c6914561017
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 2be9ef06-7cd2-4f11-913c-4ee31c1daee7
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: f4b89bd8-f028-424d-9928-e922bdbdf6b2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 5c9e8206-a923-45d5-b029-2538229af727
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 2ecfec26-fd01-4eaa-bb07-110328a85067
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: f6a0bdfa-d8b9-4d5d-b1f6-740cd75e60d1
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 1f368440-81e3-4f7f-a071-0bb10cbad874
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 338f9b3e-d5c1-4f06-baef-5d6d0f672cfd
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 096be1e3-ed20-45c2-a605-8b07ee659752
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: a41e93aa-638a-441b-9b6d-558a51f585ab
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: c527dff8-b9c8-47d0-b7f3-da97aa86b5b2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 6d664911-c30c-410d-be59-d6cf0acb2bee
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 8ebadc30-b256-4359-81bd-31678e2852f4
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: cb2d7e0c-80c4-447f-89fd-aa43ac1b61c2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 7a9b4015-1405-48b0-9517-46ff2725f715
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: d42158dd-1b95-4661-bf6b-9b1e95fdd0b8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 7c4cfeb9-0099-4c3d-a9b0-3de4ca39017c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: d3e8b6c4-e72c-4680-9134-18af6590a07f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 657d8eb7-8f9e-404b-ada1-b4c8cc98918b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 5a5f48bc-1b9f-48dd-bb85-4f96eb10dffe
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 09e12722-ffca-462b-b381-5a3d693b9dd3
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: b93dccb7-db20-47a8-8e0f-70fb1522d147
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 461f3e85-0f0b-4acb-ab59-6f18bb0810b9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 9f3650fc-9a0d-431d-a7a5-5efcc240005a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: 7aad2b6b-fd52-4732-9a8d-49aa4dd02d8f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    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: f4262773-734d-4176-9d33-e5c4ad748501
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound100.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound100.c: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound100.c
    file_hash: 04018145d5ace4c3357fe1e5023a2cdd8af65b0f762a2636eda0df151f06b137
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
