- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b0d3245-6d35-4bc2-90bd-2e0d08da9b83
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 60c3b28c-a93d-4c39-9b1f-d87c4accaea5
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 3b877ccc-4c06-4fc8-a2eb-721b9d5d3875
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 86f0f378-bc03-4134-b798-f4405b9cd9a9
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: f17ae34f-2b8b-4366-873e-afc84bba9f06
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 82b97fd6-b872-49d4-8560-f950b787bccf
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 8d8ea000-167c-42ee-be45-2d60e9bc6233
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: bc851fa2-d0ff-41fd-aa68-70bca03b0b37
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: ec141ea2-ee7a-4aa2-bbd7-f7f401ea6320
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 60db680c-124d-497e-a6f5-6dce1519c66e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 9bcd8fce-c0c5-40ce-84a6-aaa100714c8e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 1a1425d2-26b5-42a0-9976-a1e168d3ec3a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 2d936227-38de-4d34-9e35-546c90f91f8f
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 8cbad08f-d225-4f7b-a4bc-721106cee715
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 9527cd4c-d121-4cd1-8286-6fe23294b7ab
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 569bc2a6-06f4-4771-a050-fc524128531c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 4f28bf6d-8602-40a4-a621-bf105e324ed0
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: d11c0e1b-2aa1-47c3-806c-e203605e549c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: a8c007cf-6362-480f-a8a1-4ef0d58f6dc7
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 18a41333-a94b-404e-bbaa-1d6bbe5c8f26
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 61f1f295-391a-47b9-82c6-8f9c9c88ada1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 37792c34-5c88-4272-8cad-9e14516da6cf
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 53303122-4f74-4519-99fd-a3868a920599
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 7c63830a-55ec-4056-955f-f530fddb0eef
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: e256f838-932d-4238-ac20-d524a71ce4eb
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: f0ee9f5a-7535-4003-9230-bb4addb1146a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: e5c16f06-f8e6-43f6-a889-16fb07b8efb8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 03ca92a4-ff2e-44eb-897d-47760bd17121
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 76eca353-5ad2-4ce5-b6bb-562c5d02c726
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: b6592247-c7e5-4525-a9f6-3a55358596c4
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 2093671d-0044-408b-ad3d-4bb5de31b1cd
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 50dd0c86-28ba-4c12-b23c-c59dcc43f07e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 41e3250a-1ef8-497a-b0a5-85fcda83a9d7
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 38e9c53b-1907-40b9-8dfc-d27c08da81a4
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: db841180-4190-45af-82b9-c716b932364c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: bc7db2d7-ec4f-4175-a2e7-ba629d573c21
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 88b34e62-089d-4d27-9230-ffdc1afdb648
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 978f3967-d5f3-4668-b4b2-d0fc437d8685
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: f64818ff-e254-43f9-b39b-3fe6b05673fc
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 25c4f17d-4398-4f39-b6d5-5dea59d5472f
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 32fe0d38-4cf7-4fb1-be37-cbfeee4cb17d
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 64dfbdd9-7df6-4874-ae2a-9b2dc6ec0c6b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 7dfeab08-dc08-4e6d-8044-62b4fc42d399
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 042c51b5-ad31-49c9-b77a-79628d54af1b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: bf6e9e31-621f-4abe-a1df-2760a4196f55
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 398123af-0582-4e2b-b2fd-5f448e9021a6
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: ffac4609-eb5d-429c-9233-b220d5222010
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 493130c8-e75a-4e07-9bae-f5424598e10e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 94fa5ae1-d39f-467a-a28e-d96388df4482
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: cee29afa-0ea6-4795-9c49-71be2bd0e089
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: d0dfbc29-b236-4053-9037-7da739fdafd3
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 91535068-cd1a-445d-9d3d-4d0decacff0b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 9585e9dc-2a3d-426c-9015-f9cff99e2540
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 920e9868-0d39-4535-ae2c-bdb4aa380bdf
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: f73a6935-a88c-4bb3-9e4e-19dd1b2e0ea4
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: ebf0b90a-45ba-48a8-98ee-cd0aee8a3181
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 130b8a70-e53e-415b-92af-96afc50dcbdf
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: a280f4a9-3eae-4bfd-9600-cd8a127047fc
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 513da274-6d44-4ae6-bed8-32b75a91af08
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: c23a9f84-e237-4bd3-889b-129eb49c082d
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: d4c1b5d8-490f-4ed0-97f1-fd637ae9cba5
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: e7836724-a3f0-4165-b97c-375b28cbbcc1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: ced4627d-d8a4-44c3-8e22-8c739b43abd1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 4b65126f-ab31-470d-8c54-a7c5fa6bbd52
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: df0a31cb-4adb-4296-8999-0199836bc639
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 934320ea-e22b-4b40-9931-51a2b7409f58
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: eb1d0ef2-0670-4f7c-b638-ddd9df889dfb
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: d6b01e4f-69a6-4376-8452-871442452c08
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 64422d82-1311-4b73-8bd9-715435fcbb97
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: fa0e22c4-d256-4a68-b584-64b2ae386c03
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 9a8d5378-ed68-4fa2-aae6-ed324e9ea9b0
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: a5fb616a-8d2f-46c5-93d4-29beab3a6d5d
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 9ddcae27-c1fe-436b-b883-a7d760a896a1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 76d05e3d-89c3-4613-b28c-32e3edcabc13
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 876d06d8-ed5e-4f8d-b767-b849d4dd0388
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 80a20dd4-59fd-4756-836c-580708d082e8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: fb464391-707f-4fc4-881e-ba569e2ebfa6
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    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: 93cecd92-02d2-42d1-8dc5-0c9bb4b253a7
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/cohencu-ll_valuebound50.c
      input_file_hashes:
        ../plain/cohencu-ll_valuebound50.c: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/cohencu-ll_valuebound50.c
    file_hash: 0bcbcb4a55258889434b8bf703da9ec6fb29d07a2fbacad968a5ab15e005b314
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: (1LL + (long long )a) - n >= 0LL
    type: assertion
    format: C
