- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a95ec628-03f8-4d6e-9cf4-735ca8a7af03
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d5b4c4b-a1da-42f4-91ba-658a8bcedbb2
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81149e33-4d67-41e3-93f4-91709b38f42b
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afcfd890-84bd-48ae-83df-4a3561a412b4
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 34
    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: 2dc730b6-7870-4e50-a148-f83437513c35
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 35
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac0a86a3-5fb3-44f8-91c6-25969d450bdb
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 35
    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: 8a1708ae-7682-405b-b8bd-e3b09ff0a4a1
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: dfdf31ab-3e96-4abb-9e1b-67dcc1c5647a
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: ea4e4723-d087-4bad-a78c-dc7119d39c42
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 37
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19a7a378-aa33-47db-8df4-cbe3d5d48525
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088d49a8-3c9e-40ec-a91f-efb11f58fa15
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef93a8ea-0d7e-4003-8154-273b6fcd4da1
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 38
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d36c1cc-b8e2-4aaa-b131-e8dc48b27e52
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 38
    column: 12
    function: main
  location_invariant:
    string: -1LL + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2db62b0a-2d99-4895-9e33-2821b79fbfed
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 38
    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: 164ad776-d304-42d2-8eaf-d2d2ed807dcd
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 38
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d309e2ba-1f14-4ab8-89f2-2b162c1d040b
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32304bb9-ecfc-4798-9103-c484bd34b7fa
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 902d27ad-0a2b-4031-a9cb-61b8f317f510
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1181290b-7557-4480-a9d4-496ff3ad47c3
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 39
    column: 12
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64a1b453-86b3-49c8-90b9-750f4dfba3f9
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: db942581-f40a-4153-9fc8-d0cd85a75a13
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 39
    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: 965aae7b-4680-42b2-a43f-035e12840c42
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: fc9e5f24-3ec9-4ebc-8940-24d47291cf5e
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: 08318e59-e609-4b5f-823c-130c14141d46
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 41
    column: 12
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fc7862f-aec2-4ca5-82a8-7fa48be91de1
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: 610d88e3-74b9-4128-a836-869ea7f6831a
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    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: 6e033382-b439-483d-8ae7-3653f4edde90
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 41
    column: 12
    function: main
  location_invariant:
    string: 0LL - r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97439150-47ab-4e0b-844a-4439fd37100d
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 41
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a46f63a1-a98a-4b49-b809-2b7a343cc783
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2df5521-a6e5-48ed-84ba-53dc2fc15cd7
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80e7397e-4d3a-44ef-bd67-38baf57a4485
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e97555e2-0193-493f-813d-8afabb2de6ba
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 42
    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: 10750ed0-49b3-4b22-8cf4-3c7ff9ba6136
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 42
    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: cf2fbeba-815a-4108-8788-cfcfbcd5ff5b
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 47
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a3edff8-556d-4fff-ade5-9d591d3f967a
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 47
    column: 4
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d94a731b-8e18-44c5-8b4e-65aa463df510
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 47
    column: 4
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1e44c73-5cf3-43ba-9c83-c0810f2f4110
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 47
    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: b6886d7f-2a8f-4e1a-93e9-c9953178c54c
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 48
    column: 4
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cfecd5f-bcb9-4dd9-af93-f74ef1749006
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 48
    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: 0fa68d83-d948-420f-898b-8578bc0ba040
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 30
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e83bba4f-e4c4-40e7-b310-c1ce155fa8f4
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 30
    column: 4
    function: main
  location_invariant:
    string: u <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f62fb3d-98ad-4c0c-81f6-506644e003cc
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 31
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e78646a7-e6df-49b2-b599-7da83fee79ca
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 31
    column: 4
    function: main
  location_invariant:
    string: u <= 4294967295LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5085e97b-d220-40a3-aa1e-cc98e284fe67
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 917c4a2e-8028-416a-8544-89b650cd2f4d
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c944ebfe-fbfa-436c-9fbf-e650a8c41537
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d8b3501-cad2-480f-bc33-2a9d57feb026
    creation_time: 2023-01-27T16:29:29Z
    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.c'''
    task:
      input_files:
      - ../plain/fermat2-ll.c
      input_file_hashes:
        ../plain/fermat2-ll.c: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat2-ll.c
    file_hash: 43c7c57321afe9055366ca260a89f0e4de96718cc528ce2ea2543b13c4af6ed7
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
