- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf00cd05-e6ef-4b80-898d-0202ffebfdcc
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c622602-9248-445a-9910-0e8c1528b00e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3550c51-2065-4902-8735-bffa65d51c64
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7531f879-2624-41fd-9340-b526ceed0b8e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 31
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e6a916e-a3f5-4317-8788-1ae2f6586390
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ff2b080-726c-4e4e-b4ba-b986238282d8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 32
    column: 4
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac4046df-210c-4d2b-88ed-878068ed7957
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89c816d5-facf-4658-8e75-f3f19ab94b1d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 35
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1ae47fd-b7c2-40a8-b5e7-dcc696f4292b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 36
    column: 12
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8adea41-0107-4769-a233-ee1894f0b475
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 36
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 890958c0-3080-40c0-a463-91e047310a38
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 39
    column: 12
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30910e1f-d8a0-4504-8700-6f5cb9a580f0
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 39
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae3ad7bc-d28e-4435-a632-1ac302b03577
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 39
    column: 12
    function: main
  location_invariant:
    string: y != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20ad04ce-e87b-44d6-be2f-8f50dbc803ff
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 41
    column: 12
    function: main
  location_invariant:
    string: -2147483647LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c24e0202-d56b-4ff1-84f8-77cdb5cacf24
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 41
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1952b3f-51e0-4355-be89-21672a479324
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 41
    column: 12
    function: main
  location_invariant:
    string: y != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7672528-7cc4-4a14-b5eb-394c87137b20
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6786609-b31a-424e-aec5-289d685cd810
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 43
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04b9017c-35a7-491b-9348-822acdd30320
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 44
    column: 8
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e325f305-65c7-4480-bad0-58a2c6837a06
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 44
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: caac821c-5009-437a-b208-5a108d686f2b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e2e4b71-c6ab-4511-b8b5-7151d1527f62
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 25
    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: bdb540d4-3fc6-4b2f-b27c-336ea4dfdd77
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 225bb984-4bf5-492f-a8e5-3429c8d8c8df
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prodbin-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound1.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound1.c: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound1.c
    file_hash: bf6b5d6ce0125c606cfafa6fb4e25513c25265a3f4d4cd63094ae1ba72acdc4a
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
