- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bc6d238-6faa-4034-980b-6ec00681fbfe
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 70fad181-ae03-411e-b506-a4a4e06e0f0d
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e51f39b-83fa-49ec-a781-95934d6451da
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 98410819-e1cb-4684-ad52-78ff7503d8cb
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 34
    column: 8
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: accf3652-1f08-4c48-96e6-d90c0882b21a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 59c2c5aa-815b-4cce-b93c-041cca2cfb33
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: b92db7de-b29a-41cf-82e4-0bf41898fae6
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a35d4ea-942a-4f72-a042-80cc4d64e191
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 825053d7-b50c-4e64-a206-6181a75304b4
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 00b5b377-99f2-4e80-b254-f0f863730a31
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62061f98-bf5e-4617-9ee2-725552ff1053
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27e1b379-3170-42e2-948c-c98f438504c9
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 36
    column: 8
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c2e8c3a-dcba-46e2-a7b8-3e7ec57a0026
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 36
    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: 3838f001-b9ce-4ee9-a616-c0f58fe42228
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 37
    column: 1
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70d3cd94-311f-4a69-ab08-85607c644f73
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: af83b144-d4bb-4cba-a57f-cc945c729c7e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 63f35d16-887a-416a-affc-621aac9f4086
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: bb80e8ed-934e-4c47-b416-7cd8a561702a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 6cfe6061-c3b6-429c-871e-3bc006a37657
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b76ef00-eefc-4676-81bf-2f88be130044
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 38
    column: 1
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32dd0be0-6cc0-402d-9d86-0f686cf867ad
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 38
    column: 1
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf796032-4310-445c-abb6-2e19d2cb9eaf
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 38
    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: ce5f08c3-24ce-4efe-b614-44fb3fe83075
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 39
    column: 12
    function: main
  location_invariant:
    string: (short)0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdb445e4-5ca3-40de-834c-8db9dbf6decb
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9462727a-b72f-495b-89da-7691ae1ff82e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 39
    column: 12
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d62a0e0c-a80e-4a7c-a2f6-81ea3b94e231
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 39
    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: b9c71074-b1c7-4188-96ec-8cb2e281eaea
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4a05ac5-01db-40af-933f-737062ce7458
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 42
    column: 8
    function: main
  location_invariant:
    string: n <= 32767LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55308cb1-f356-4320-833b-4ad3baa5646a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 42
    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: 99738d2d-78fc-4c83-877b-dea453302c33
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6242edaf-506f-43f0-aa76-5ff4988aa1f2
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 1LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 300c07ce-97ce-4d2f-a72e-1ef1627a50e9
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 9aabb5d9-0a21-42bd-8c67-f68cbe584792
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 43
    column: 8
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c74a5598-c528-4faa-a716-1f9d7f5ba1d7
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 240dcb39-8d2f-4290-8640-e4df1641a086
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 1LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6ccdc07-2bbd-468c-8652-73182afe9c82
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec5d456b-eafb-401c-8547-f1efb2f3d8ca
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 5fba8f94-bdce-4751-b484-5be110a0e24d
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 148aeb77-ad90-4d7f-854a-9431cac4f916
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 94c2b177-3eac-41b9-b200-7385d1c408ea
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 404b8857-85c7-49b9-ba08-0e3c9414ff49
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 7LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01c990a4-1d4c-4fec-a1a1-1c6eebfdcd1c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 45
    column: 8
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d78e32ac-f513-43a7-b818-1a1baa6b369c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 45
    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: 6c76951f-c5b0-484f-8425-c5d642b42ca3
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 1LL <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa981ca3-4f14-4e30-b4c4-af01caefd5a1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 1b24a9b4-4fe1-4b0a-a87f-909017b44058
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 48
    column: 4
    function: main
  location_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebb6a25c-7645-40e6-90d7-3ad8320cd016
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: eda7bd64-b38c-4fc2-b564-3dd1541032b6
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 48
    column: 4
    function: main
  location_invariant:
    string: n != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11d70c66-4c01-4ff7-9779-6f9929ba03f8
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (short)0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 492670dd-2326-449c-ae0f-458aef89d159
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc657711-d7c8-4443-b050-87ce957408b4
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 21ed476e-a970-4b58-b558-ef4113a57b61
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 5e21f99e-d4ee-4958-b118-625dc338a94f
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (short)0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94a572aa-9dd1-401f-87cc-a6cc0ea908f1
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 992c731c-9cbd-47b3-a371-c6ccbc23cccc
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: b6904f05-7684-4007-98e8-d59fd9344f91
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: e47d3b65-b558-452f-bd56-59d4673b25ee
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 066b5875-638d-4b5c-ab81-ab358bfb052a
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 7609eac1-d485-4d76-8f39-2c226d728179
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: af2696fd-f173-4ea6-a817-41b5f560eb06
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 48170568-5099-47a7-86ab-023a6150a016
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 8432f7d1-6718-4060-81c6-0bdf7d4ab88d
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 8b7e9147-27ac-48a7-bb0d-488d69fe42c9
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    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: 6d0fd698-3f47-48b5-bc7b-efb844e4ddda
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 53
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98cf5718-a7bb-49dd-85a0-2c3648d5365e
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 53
    column: 4
    function: main
  location_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19a689c6-c253-499f-9263-3a69d46478c2
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 53
    column: 4
    function: main
  location_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e972b55-8d89-4c73-8038-6f2d85378bf2
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 53
    column: 4
    function: main
  location_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a94f1eb-e74f-4e02-bdbe-712d2e47076c
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (short)0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9f842fb-e11e-4390-a4a8-57d19843a393
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 26
    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: bcd2514c-e45b-4709-b779-73e6e86151be
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 26
    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: 94011b82-c1cb-45ca-91be-fc83968d194f
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: (short)0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 84750c94-f622-4b6a-8f6e-56c4c48a1deb
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 08f5d75f-ff43-4cb5-9d53-9550b6b9e012
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b712be5-bb9d-4fa5-a9f5-979527707af7
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 707bfd45-388a-4da6-805d-0e3fed3bad73
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 6LL <= z
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26633bc8-790d-412b-8c85-882ec1480c47
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: n <= 32768LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 51648456-c46e-4d18-b825-06349361fe58
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: z <= 393222LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9e6dcdf-0296-4907-9b2f-929bf38d5ab7
    creation_time: 2023-01-27T16:29:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound2.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound2.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound2.c: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound2.c
    file_hash: 942b28ff7c0583b7db8395d2c315e70afc8fe68ba69d39faf867ac75d7628edb
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
