- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64277d89-4bd3-4486-974c-9f7903ad0afe
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8273166-12dd-4d56-884f-32b328b8c467
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8785e978-2e03-4356-a24c-2ec8fa84096f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 33
    column: 8
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c982c7f-bedf-4aab-a5c3-496521915269
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 33
    column: 8
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e059213-7ba9-43e1-b484-304587f870b9
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa3d349b-4d17-4fd7-816e-8182fdd47e58
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4076b20d-e3c2-4796-ad48-1aa08812fd6b
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a13e4b0-a3a9-4277-a0f3-2c70392678ed
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfdcd121-e494-4aeb-93fc-786b8513e9c1
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 34
    column: 8
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc4b0137-934f-41b9-a22b-050c3f2f9248
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81c3afdc-ae7e-4592-b7c3-d81fe79e881f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 34
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eae0c935-8907-4028-969a-b652722ea0fb
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 298076a8-888f-4d5f-bf32-f53a71d26ef0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87f1e3db-41e7-46f7-b4ef-d738eeb170a8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc85f829-9bb1-47da-8fa7-de5e1e0aadee
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15c707be-c6aa-4a32-8518-800db3fd7ef8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3986bb05-11c7-4db3-871d-001ec1ad933f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 36
    column: 1
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7956e00-c48c-49b5-8dd1-21e022c93bde
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 36
    column: 1
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b0fe7e2-2320-4e0f-9d7c-bcdd6b1ba05e
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 36
    column: 1
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17cd37bb-d578-4fbd-aa3e-607475eb25b0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 36
    column: 1
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27f4dd0b-1948-40d1-b9c6-b6e9e60dde66
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 36
    column: 1
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43b2ccf3-7586-4247-b28a-8343ff1e90d2
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 36
    column: 1
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68d9455e-0fc3-4f28-84ab-7d04902ec1bc
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 37
    column: 1
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7bf5a8d-1efe-4340-b9f6-81ec42f44d13
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 37
    column: 1
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0cf0cdb-50ce-40cf-a213-f8306a6e4514
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 37
    column: 1
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6be49639-68e9-4a98-bf7d-571b5d6a1f64
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 37
    column: 1
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38772fca-ba88-423b-a531-c8e079b464df
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 37
    column: 1
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04ed4c56-c393-49a3-9993-865b4b31ce3e
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c682884-9dd2-4611-ace1-e40bce46276e
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 38
    column: 12
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0cb97ac-e37a-4b8e-919a-ba13629d98a1
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5be0666c-a585-4483-ab8f-2e3389e3681a
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 38
    column: 12
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6908d686-fdde-4806-842f-a07a6465e7c3
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d16d532-edb5-4a28-b545-0c8d30e77e4c
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 41
    column: 8
    function: main
  location_invariant:
    string: n <= 32767LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2b8cf55-fc0f-4580-ae6e-11a623b52708
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ffe5df0-8626-47e0-8093-540924d955e1
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (long long )a - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 013e64bb-1c66-458a-9ef7-72c604295676
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17862997-4850-4cf3-a322-dd91ec983bed
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 1LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a491c534-c35e-48af-ae2e-a705a954ef43
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdb048bf-d968-44e1-b480-3c80903d516f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3b49659-56a2-465c-b1dd-f48d3c58de91
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09d47930-e2d8-4d76-9821-e1f8f5f1a2c5
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0c1dc7f-e3e9-4751-b0ac-94bb8056331f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 1LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b97e6b99-8308-449b-9077-f064874280b0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a303c1e3-7e7b-4e66-8d08-6b385f8e75f5
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4fcbe54-ad58-4b56-8248-7a96a4f1b798
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 43
    column: 8
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf6d48c6-3bbd-4639-b6ea-f65f01cee51d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6cf70c2-f0df-4bb5-bcd9-4b4d260a3c6c
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a44b9541-0a2d-4861-bb06-c7eb982ddd6d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0b084f1-41ca-4251-a2b2-afa2204557cb
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 7LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6661dd58-dd29-43de-a2ff-b70499a897ce
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 44
    column: 8
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39aa59f6-5261-4f98-ad8a-4de684d26336
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d16c99fd-4f21-4e40-8f5d-9e2ce0e80dc7
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 44
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2dfaa6a-b35a-410b-9c9d-745f5aa27245
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 47
    column: 4
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0eaf227-cf9d-47d4-b981-1dda8d097e49
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 47
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 897103d4-2f00-4051-a04a-3574113e0716
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 47
    column: 4
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7c7f0af-0e36-49af-b525-a479a4a9bc31
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 47
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 563cc116-e616-4718-963d-58f48b1bd5a2
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 47
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d066fa8-5d79-40a8-9a29-6d9083a84d4c
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b212cff7-e9d7-48e6-adb9-21f335a235c8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52f64dd8-2cbd-4867-9a81-4d7ca2622859
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 48
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6aa9fca-4e2d-49a3-922f-b851e3dd11e0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38c061f0-1a52-4b3d-8699-83a7aa76dcda
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f9e6148-8ce2-435d-9643-b5421d411153
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f824bcf-b9c9-4cad-8cfa-edf8830ff6c8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 49
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 473763ee-e16c-4bbf-916b-f5a7472b5c7f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c739e81e-264e-4a19-a877-f2e0928b98b8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22212c89-b9d5-457f-9e74-d109d4610015
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d1c784d-a678-4d03-9158-aa2b259f844d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ce1163f-fcda-4ced-8eb5-4ff2c65d8b69
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 50
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b465248a-6c23-4bbf-b973-eb8f3090264c
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dbfbf23-6420-4858-b563-ba3a0e58e3a0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c2a04a5-8815-46c8-ad55-065e5ad0e672
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d378cc0f-3c7e-40c7-ac52-593d1f48e5ae
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 51
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99b307be-a85a-49a3-a4e9-2d5375eb4678
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12d062f5-9ae0-48ea-a9f6-c8d2395fe18f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 52
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3a01497-4791-4441-add8-1875bb16e4af
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 52
    column: 4
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f785dc50-e50d-4830-b1db-1252f645d4c6
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 52
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03c292d7-e3d9-4415-b4fd-e6c92968666f
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 52
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 558fba1e-1f45-481a-9294-28fd77f8c36c
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 52
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 079020ca-afe2-4aa8-875e-aa85b08bf0de
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 54
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eedd1899-3c86-4198-a20e-cc8127591086
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 144f8f0a-0535-45d9-8aaa-4b6be6705a5c
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17daf8a5-0ef2-432e-a53b-148735e34669
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa3f8f12-fe10-42a8-b136-334a1c2fb5d8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec227ef7-3715-43cf-bc08-736309144bf0
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d43cc2e8-2a01-47c8-84a6-ab7e98097040
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e57fb18b-25aa-4ef0-8e14-9f13cae266d7
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 090c3060-349d-4a32-a6e0-4720a19131ad
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 651e10ec-bdd2-46b4-a80b-d904657cfba4
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 87f842bc-5ed4-4725-a492-3996ae2b1389
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c56892b3-d260-4da2-aa96-bf56b9fe44e8
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 36ce055d-7948-4d71-b939-cd54ce048a1e
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d8feaf5-84e6-4567-a8d0-f55dfb0f6126
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6db146c5-1a22-4b9c-8f6f-b1b8152b610a
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eeecc280-1c21-4d9c-98f4-05fd2708c13d
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 65535LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f8c7d76d-3058-4b8d-8467-478c9b4ded9e
    creation_time: 2023-01-27T16:29:19Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/cohencu-ll.c'''
    task:
      input_files:
      - ../plain/cohencu-ll.c
      input_file_hashes:
        ../plain/cohencu-ll.c: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll.c
    file_hash: bf57d72e341b105161cbeacf29e58db93d2b67f8e0e097e4dbed74551cbdcfff
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
