- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb70dac4-cc03-4f8c-9fb5-a535ce236215
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 08419812-52f2-43ea-ac82-e62983149307
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: b37fc3c1-77e5-4963-95c7-53308f70d713
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: acd65781-6194-4efa-84b0-eaa4022751ca
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 0913c264-777c-4527-9dcb-1f625e4a81cf
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: b7fb161c-c55f-439c-80e9-ae8891331cb1
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 13f378c7-71d4-4d68-9299-e597f3416d7a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 8a2420c0-8777-4f8a-9357-387f9370c3e0
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 341f09ab-1b3e-4b43-b977-0d0a22b2889f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 6f3987dd-fcdf-4108-b395-6f17a37c34a9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 3ebb71ca-27b8-4e12-88f7-c0b5336d7069
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 6e40ab8a-c81a-469f-a37a-05c4b7d2e8a6
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 2df21b26-456b-48c3-aaf4-baa21cfa22fb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 24fae967-9c05-4d29-b44f-cbbae6a859a7
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 66b7a2ba-809d-46a3-80cc-28f6793459ec
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 89b2e4e5-b003-4406-8ec8-ff6df3b9b672
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: e0a4a35b-80d1-4866-af11-679588f4bce4
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 795cfa47-b27f-48eb-b961-00376e473532
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 7bcb5dfc-7993-49a9-8b9c-a32e882b69fd
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 421ab3da-1528-4dc6-a613-1345717d4486
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: b9e04a2b-b482-4acb-aa15-0da46fa52d23
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 7da7a766-da9c-43fb-8ca7-c4b1fb6ce05c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: 21b3f879-6dbe-44e9-9bfa-d63fc9397b2f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    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: f4d60cb3-a165-431d-b3a7-3aa97efa5c69
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prodbin-ll_valuebound100.c
      input_file_hashes:
        ../plain/prodbin-ll_valuebound100.c: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll_valuebound100.c
    file_hash: 8bd25fcd8e8d81d9ce03f11651b22e7d6f0ec0da3b511f7ebe00128a9109f319
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
