- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dde9a5c-22ff-487d-b26a-c8c41dfef0fb
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -4611686018427387903LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1141caf-df2f-497a-a9ec-8be42e5a14ed
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 01f5666a-0bec-49f1-a325-205d530e78e1
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: dbceefde-cbc4-4a05-8555-d524defa3058
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 34
    column: 8
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da5cc2a1-44a7-435b-b3b4-78d99f723b9f
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 1cd74c21-ed5d-4fd7-b482-f5f1115ac752
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: ec4f2756-a8b9-4027-99ec-35838bec8ce0
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 35
    column: 12
    function: main
  location_invariant:
    string: -4611686018427387903LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc7c59ea-a7f6-482d-8cee-bf77e1896a5d
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 35
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34d88b22-d19f-48f9-9c3e-7a7bbccae835
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 35
    column: 12
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5c738b4-4fbb-49b5-be98-3b6f4bc4d5cf
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 8c07f748-5f31-4611-9eea-4d937297aee0
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: ca7dd66c-f94b-4785-b257-269fa0f3e30d
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7767d8a7-2f57-48c4-8a94-45131b909078
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97d51262-8845-45ca-accd-167f41cee3c2
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 382c95ff-a350-4c29-9e26-75331d75a514
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3926d9d-0ce0-47f6-bd03-349238ae8fea
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8a606ca-f454-4815-9be2-26fffba75cc5
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 39
    column: 5
    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: 9130d010-2690-4b97-90e5-810fe3122f81
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 40
    column: 16
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c48ad165-0fcf-49d2-951d-173a76cf7678
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 40
    column: 16
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c45095c5-a6b2-4659-b1c7-bf3e8ae17e77
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 40
    column: 16
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e28abfe8-7b50-48a9-aa3c-8c8d713908ed
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 40
    column: 16
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d1ce01e-f29e-48bb-86f6-2d8776cb3819
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 40
    column: 16
    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: 5668d65f-a052-4666-9a4c-7bae821ae109
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: d32c2c34-6027-48d1-85ba-d59e0012a25b
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 1LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf56b22c-1317-4341-b5dd-e53c5fe53039
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 42
    column: 12
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9da4caad-f4e5-44eb-85cc-2798e434ed9e
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 580ae770-979f-47d0-857f-843a753a165c
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -1LL + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef93351b-1135-4636-b3d4-c5acf2d5d43b
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: be492763-8e66-44fe-a685-d4722f8eda03
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 42
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb94f134-3cfb-4d0c-8d7e-3e0d31a50679
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62acb195-fd64-4b6d-84da-d67c67c7aed6
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2dc41589-201b-4369-9f31-72813e619dd1
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 43
    column: 12
    function: main
  location_invariant:
    string: r <= 9223372036854775805LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10bbaa6a-fc85-4428-ad8e-cd56f64f6d8e
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 58c40f43-3488-4f86-805d-b0f056e09afc
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 43
    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: 95684be6-a94e-4f36-aa49-3c8186e6168b
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 8f5a6ce0-a708-408f-a319-e12fdd23396a
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 47
    column: 5
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 861d1219-a197-4a7e-80ca-8c0abf0b7906
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 47
    column: 5
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0be14590-5bb5-4f5b-88a0-9f8ba6ac959a
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 47
    column: 5
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90659918-ccdf-4499-98d0-4be580a31d32
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 47
    column: 5
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ad8b8c9-5276-4130-b6ba-5ce88c3ebd5a
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 47
    column: 5
    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: 4f91e7b7-a446-48f0-8c27-8d3a7ae19eff
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 48
    column: 16
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e375c17-58d1-4f4f-b482-df0b81a8d1b3
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 48
    column: 16
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a2e110e-3e2d-447f-aad2-091a09ee9990
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 48
    column: 16
    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: 98c13c83-ddcb-49ce-8de9-82ad96eff434
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 50
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e35eaad4-9921-4e9e-8529-9097272c7f7d
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 50
    column: 12
    function: main
  location_invariant:
    string: r <= -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad9aba23-8207-4fec-bb9b-b2c14043e817
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 50
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ab50647-39f0-4e55-9cbe-271905b176e4
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 50
    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: 3c1d409a-d8f3-4d95-8022-5e5141eb7387
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 50
    column: 12
    function: main
  location_invariant:
    string: -1LL - r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea94c809-8ac6-426d-bcde-cc0279b6a4a3
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 50
    column: 12
    function: main
  location_invariant:
    string: r != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38f608b2-8d1c-4618-a2ae-17bb6a26b7c8
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 51
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 210df7a4-b120-4eff-a453-7e96b6ce5282
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 51
    column: 12
    function: main
  location_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf0e8158-3f01-4119-9baa-941016945640
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 51
    column: 12
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 674f4552-0dd8-409c-83bb-cf6e3fd0dbb8
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 51
    column: 12
    function: main
  location_invariant:
    string: (-1LL - r) + u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e112ee50-5b6d-4c04-b7ab-fd9c2b4cd4d1
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 51
    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: 0b497771-7294-45d1-b073-491275bcfaad
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 55
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 990233fb-8f2a-424e-8bb7-aca5d54331e8
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 55
    column: 4
    function: main
  location_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68631945-8ffe-4795-b94d-d3c994c185ce
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 55
    column: 4
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9437cdff-4771-40b3-8dfd-282eaf4585fa
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 55
    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: 8e5db103-2839-40e7-912f-36effcbae5c6
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 56
    column: 4
    function: main
  location_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca4dfcf9-9cb4-4dc3-b939-3a2324b455cf
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 56
    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: 06c863bc-d693-4f7a-b720-ac85de6fba3d
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 29
    column: 4
    function: main
  location_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fbbeb54-b453-46e8-a6e3-a8d36d7bf757
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 29
    column: 4
    function: main
  location_invariant:
    string: u <= 4294967295LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8f640a8-a21a-4959-9339-93a163670ad5
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -4611686018427387903LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f31dfdee-44a5-439c-8403-41213df90968
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 690d5fdc-b81e-4322-98d3-36695b82b8ce
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: f40f8245-c090-41c2-9d10-fed7aef616d2
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e2d10700-588e-4007-9b8e-4028f6efaec6
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    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: 2ea1348d-4aea-44dd-a001-27bc786a723c
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 948fd7d7-3eb2-425d-b6a0-438de8d8265e
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 38
    column: 15
    function: main
  loop_invariant:
    string: -9223372036854775806LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f32e406-4636-48dd-b474-db8700fc0104
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 38
    column: 15
    function: main
  loop_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8b57558-aa13-49bb-acf2-585cf7eab72a
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 38
    column: 15
    function: main
  loop_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b99679af-e615-43a6-99e0-3c44ef6d93ec
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 38
    column: 15
    function: main
  loop_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 478d9429-865b-46fb-b73b-37d1fbbb234e
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 38
    column: 15
    function: main
  loop_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77bd70ea-434f-4edd-8883-7d95658edb4d
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 38
    column: 15
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 625a3093-d47c-4f75-a642-f383dd3ca050
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 46
    column: 15
    function: main
  loop_invariant:
    string: -4294967295LL <= u
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 926b3764-eb02-4434-8019-6d4cd05d40cf
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 46
    column: 15
    function: main
  loop_invariant:
    string: 1LL <= v
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe13862d-7606-4324-97bb-118fa14f71c9
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 46
    column: 15
    function: main
  loop_invariant:
    string: r <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9fc5ec1-ee07-42b9-be74-56d5d62cf5b5
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 46
    column: 15
    function: main
  loop_invariant:
    string: -1LL + v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bf8d46de-d77e-48f6-a687-82a8b4a13738
    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/fermat1-ll.c'''
    task:
      input_files:
      - ../plain/fermat1-ll.c
      input_file_hashes:
        ../plain/fermat1-ll.c: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/fermat1-ll.c
    file_hash: c5787d4099664297951b30a30ca371dd536df07843738ed8698fe723430a974c
    line: 46
    column: 15
    function: main
  loop_invariant:
    string: (-1LL - 2LL * (long long )R) + u >= 0LL
    type: assertion
    format: C
