- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 462f0e80-11b6-443f-aef1-2c8b76af5020
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 30d70cc9-a61e-4f8b-9d69-5fc2a9681519
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: b0613e57-646f-49ea-9b4c-e68fedb3ee79
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 7f2698b6-8a49-4e77-bd33-b7187dec324d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: eda13f21-d6e8-408e-ab5b-172c69a6d45f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 22085d30-9ffc-4ff0-8602-b5406d576b52
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 8791dedf-4ea6-4687-8a34-8f2785a31766
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: abd21eaf-88d2-484c-9e6a-49d9218a6377
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: ae4c467a-c434-44c0-a7c5-aef73a0a0dcb
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 765e3da1-5803-439f-87f4-b157d19d5fc7
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 1837242b-fff7-4cab-a33e-7553550a0819
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 338fe4ac-1913-4558-ae90-298f7964878d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 91293855-38fd-4764-84b8-0561def7469e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: b8c72bfe-368e-4596-b4d5-b8ce57fdcb9b
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: cc9d6a5f-d78f-4fe3-b1f7-ebc1429b2188
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 0b6dc0a7-3426-473c-9eb4-1ade5d581931
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 81cfb547-d620-481e-8302-ad06acccb5a7
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: a3aa75ff-dd8a-472e-9f4e-a29715cd96df
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 3c60be34-b20a-4898-a6a2-462cda8fd355
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 04eb4e18-8c60-48d1-adfc-3c9410c3d822
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 30fa8c84-f66d-43fb-b7cb-412bc9891a0a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 35bfb740-6cb8-4261-aa73-9b890925e776
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 3cc05827-e9c8-4196-8666-4ab67b119b39
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 43d16df9-e272-4365-8b96-90aa2c9adcb3
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 50a77d38-974c-47c0-8c87-c36afa43f175
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 97f3344c-c2de-4713-aa84-4c9d3fd8b798
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: e98f3ed4-2eb3-49b7-a1aa-88c4299a3afa
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: a1d9a980-95d8-445f-b66e-656c1f6846b1
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: a5216538-9ee3-4548-8137-6b2e7c17545b
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: c7992a7b-8378-4784-a985-b9a470208682
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: ec9e2454-33de-4dff-9493-89579886461d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 22706c1c-eaa2-432c-8f8e-20464dd6a649
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: f2570e42-fcf6-4048-b4a2-4e3bb4adc3a0
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 75ba56d8-c272-4515-bbfc-220eea760759
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 8a82c89d-04d8-4098-a134-74ef6305fd2f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: ae02e1f2-3077-4941-b40b-3cfe7ffd94e6
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 15769933-6103-475a-b8b7-2a9dd3610831
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 3cad00f2-9e1f-40c3-9594-2b03b8ba7b47
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 5e23768c-ede6-4d86-a76a-5cb6c1b68e65
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 76c2eea7-583a-4320-96fa-dd52783a6445
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: ddf2fef2-0541-422d-9a8a-9155a5948ae6
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: e8ce1100-36bf-47e7-9ec4-009ea3c2509d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: b5566c1a-603c-4f5e-b6ef-23a504014e1d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: ee88eb96-a9f7-4744-8441-6ee848d9d258
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: de012b30-e6e8-4794-99e9-09a054d3bb1a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 25e8d0fb-c6c6-462f-a48d-ae015ee34da8
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 0648bbd3-2376-414d-9611-7d270a8fe48b
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 8a5c0308-3015-4346-9fed-e97a9862b6d4
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 7f4ac0af-f58b-4de3-b4f4-6777a7de0b4c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 9d40a470-76d2-472b-bf14-54ee022582ae
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    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: 461b3384-5a65-4b5b-8ee0-c6d66144129a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/fermat2-ll_valuebound5.c
      input_file_hashes:
        ../plain/fermat2-ll_valuebound5.c: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll_valuebound5.c
    file_hash: 26b0e9a1f24f001efea295bcd9797908bff3501d4b08818e2be1159233981d8d
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
