- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b32565d-5f94-49f4-9932-0f4b0884a3d2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f803019-a7b7-413d-8146-ed7a3c045fb4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98f7215c-f592-40ee-9c58-3c9260e72982
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31b3059a-ca61-4ec9-9b01-6e6e2fec40f2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 30
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41f59969-afc4-429b-937b-b3a3415c96fe
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff7c774c-2288-4ec4-8907-be94f9c212c1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 31
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 233a536e-e2d0-4f2a-967a-d2aef4264896
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc01a596-4ac4-4544-ae9a-50353b729f4f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e98d190e-1296-42bd-86a5-54b13dd70390
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 32
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a6005fd-db5e-41b0-a79d-c8f409e21691
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 32
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bccd3c22-c5ae-495f-a48f-c0169c7c870c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1300f50-dc0b-4444-9755-970e10424dcc
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 35
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8041f124-e10a-4eab-a128-be8bb6d605a9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 35
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf8d7c20-f737-4a76-82a3-00dafa375abd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d502e96e-587b-41d2-ae13-0439d5400930
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4485ed7a-0fca-4e8f-9557-1264df247608
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 080ec50f-f0c4-43e2-b3cc-6ce58883235d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4460b12-13e0-4971-8a56-defb49be68a6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25cebf04-8cb5-4777-bc7b-5bd063302006
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5365dd6-9f12-47de-809c-8c25e1d7f08a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e1d72d2-de47-4611-99f6-43b61de65166
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 37
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7fdeb7a-4a9c-46c7-939e-8a90f38ef5eb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a39aa52-ead0-4b5e-bb45-5ceadcae2655
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a39e2ed7-2716-47cd-8b3b-9efe0cb5fff2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45341962-c5f7-4c7b-a92f-b63876931721
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e708a36b-8fd8-469b-a5b3-160d72cd4311
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 421079db-2c3c-4557-bb36-5a80d5682926
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 647453d5-edb0-4875-8a17-09a8270ec450
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a532e830-4c8a-4ec6-b640-af5d8f1a5a83
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a235eba-2ae4-4840-93a3-719e9fce2f13
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee295f12-d42b-4d40-bd62-84b5108e1901
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c3e0fa8-e7ea-4d88-8085-1c4cd1fc62d8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 41
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 000f73b3-5a15-46a9-b8cb-c6e929e974c1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 41
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 495f2bab-5e24-4d18-b433-0d6af4b7df7c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 41
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7feffa81-5afe-43f8-8a87-28bb4d645682
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -4611686018427387904LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8b764c6-e855-4229-825a-9a611905a7c0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 42
    column: 12
    function: main
  location_invariant:
    string: a <= 1073741823LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 131c1266-b937-489b-b287-425bd4510922
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 42
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e119855-6b4b-49f2-a91d-45205b8571f7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c64cafc9-fc23-4d23-b072-1e4ff3d4c67a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 42
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17f42d78-abb5-4c88-a39f-d377c227ac77
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -4611686018427387904LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37a00a35-1adf-4dca-b7fd-6f9127f7ed60
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -4611686018427387904LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44ac7bbc-8b90-4424-9f4b-daca6a28731a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dff7ad1-03fd-4fee-a83e-54f0583fd4ac
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: a <= 1073741823LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b3188fe-6bad-4b0a-9237-12e8472e8e1c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: b <= 1073741823LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf56a983-abd3-44cb-b12f-319166d60f70
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 336ab0a7-4e2c-4575-b633-de44ed37d544
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 572f680e-8960-475d-8074-792c177532e8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff7ce5b6-65b3-4a3e-8613-d3721f2ccf8c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf2bbc96-6ac6-49b7-9921-42269ad96750
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1f95ce2-2dac-4a39-bbde-cb4f2ae7c7c2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a510f93d-025f-481c-884b-a736f25842de
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34108c5e-848f-4678-9c4c-9c125bd52d4e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22f1bf0d-bbf8-4639-a7d4-3a39dfa1a931
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fe7ddc5-80e2-4ab0-a3a4-07216c1236cc
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4bdc5ba-9769-4e99-aba1-d8b36970c2b6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39a76642-a530-4db5-8b5d-ddc644a2549a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 44
    column: 19
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 062d945a-5f25-4bab-9f35-3d7938df0637
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 980d4241-99ec-41bb-97f8-08ab63113243
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27cbf0cd-5673-474a-9dce-cbb0f366066c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 675d5509-52a4-4f80-94a2-24da3ee19fbc
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3c536c3-eb71-4dde-8a75-35f5cbbf7c2c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79c79d62-a9c5-475a-85f0-d7d84f361e23
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 46
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7daaf45b-b123-4cd0-a7ab-c1c09012a986
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 46
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32285d9e-c83a-4e6b-a96d-27ead7aa4f95
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 46
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af2a16ff-4bd3-406e-bafb-7a813aded3bf
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 46
    column: 12
    function: main
  location_invariant:
    string: a != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb29a524-f5be-4c95-abf3-7c320c95b6f5
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 46
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd63364f-6b67-4073-8949-4fbabad73f66
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 47
    column: 19
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9859e8d8-26c3-4e06-b7df-02be28b7f486
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 47
    column: 19
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a130bebe-43e1-490b-a3aa-2c760fd3e8d3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 47
    column: 19
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce51dbf8-7ed0-48e2-ac96-0613618e0844
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 47
    column: 19
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7f2ffc5-7cba-4a89-94ee-f7353a5c10f7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 47
    column: 19
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c58577a8-1517-42ff-b66a-f491bf3ca538
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 47
    column: 19
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ebd2336-0dfc-47a7-865b-3f369985c5dd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 48
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775807LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5101df5-0a0c-419b-96d2-84dd6f1571af
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 48
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2eaf303a-f9f8-4f3d-a3b1-08f681d7caa4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 48
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8afe60cd-9dae-4c6b-a37a-4b66d1e4f020
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 48
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c96d2fe9-e7be-4145-8670-37c2fa8cdf2f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 49
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d55ae414-f1de-4f1f-9b5f-66a425ccc825
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 49
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3792d1ed-e3e6-4b53-9eec-fe6584f61720
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 49
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 760e1247-54fe-420f-84b5-3812e257d743
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 49
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44017d1a-2e01-452e-9b90-ff5b129708c6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 49
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87977d52-7b1b-4a50-918c-a699b4a76bc8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 49
    column: 12
    function: main
  location_invariant:
    string: b != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: baa6466a-8346-4ccd-b852-b3d32f748133
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 51
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efec05fa-67e0-43b8-a64c-1e48f8eb7403
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 51
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6936821c-9ddd-4b7d-a2b6-6b215c14cf33
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 51
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47cf89a3-070b-4c73-a605-07f43610e886
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483645LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c42c117-9f2b-4f94-88a8-4cab61e44633
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4339170-7f3c-4098-a0eb-5227873361e4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 332377d5-9725-467c-b7e2-ac8c787f9355
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: a != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3c547d7-d0ec-4856-8254-df1ed1144a18
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e41132af-8a80-4c29-b052-169b98c3f39f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c35154f-fd8a-4bc6-9897-0ab8179efafc
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483645LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 681e53cb-bddc-436f-802b-d2295df4252a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483645LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7d9ac38-b7d7-4241-88d2-ef691bc7b8ba
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ad18f1e-8b57-4280-9ce4-43c1da98f07b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: a != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f88b5bbc-6225-4843-bb87-5879b0f3ef04
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: b != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ee7cea1-193d-490f-8290-870a89267c1f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 51
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5be2352c-d440-4fdf-93a5-d768f9ee144b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 51
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c13003e0-9d8f-4153-84a9-2fa8b2058e41
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 51
    column: 12
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 614deec5-71d2-409f-ba99-84dc4a6f0271
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d80f125-a27c-4f75-85df-3688b55809f3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e28dd199-16dc-4bed-88b4-3bc91f1c6d50
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 233ac2e8-e459-476b-81b1-47b8a7250386
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: a != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f43dec35-a012-4d9b-a0ff-121803cca723
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 52
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0625b1fa-e7da-4025-ba70-7fcec4f65f6d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf120e80-d845-4653-9d56-1667741dd4c6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1fcfb0d-e316-4383-aa29-d5ef8f2a82ba
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94daac97-a70e-47a7-8ea6-63f43d62443f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4329e46-0e03-4abe-8b8a-31e8aa36d0f2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: a != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9b69bec-db7b-4186-8149-4252b218b344
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 53
    column: 12
    function: main
  location_invariant:
    string: b != -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f7154cb-9683-437c-ab81-5fe5baeeed35
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 57
    column: 4
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7eda001-b58a-41f7-9bb7-7cdf0b6f6967
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 58
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d054e08d-13d8-46f6-ab97-525549f155e0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 58
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0f4c787-bf06-4b02-a859-56524e8906c4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 58
    column: 4
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 277da1ef-d2b0-4dd1-9a0d-16c08dfd9fce
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 59
    column: 4
    function: main
  location_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e717dbbb-9e76-4124-9b4c-fb600e39a31f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8157589a-499a-4a28-80ed-99ddf57cb581
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d13293d3-d0b7-4a97-9cde-5fe047a777c6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe41a854-fcee-4d2d-85ba-3bdbd5b49b88
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3113310b-03cb-4842-864a-3800048d2141
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d77a9623-591d-4775-ae1c-f32ec02e63d2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound2.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound2.c: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound2.c
    file_hash: deafb53b6c5560bead535ea0c1ac7bb85be5c959b9a13b21177e05987440264a
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
