- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cca566cf-aad2-48a3-80c7-498a28619393
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 19a24e1a-d92a-4987-8078-8b46da362f9d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 25f963fd-2827-47c3-b624-fa42f7517211
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: aeb95e32-6ff9-4fb7-a47b-6452511a3190
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: c975e688-4f85-4689-889d-10ae7ec7f2b5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: d1eafce9-9d76-4487-b27e-ab718e3f71dc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 300b7dc3-ada5-4a5b-af5c-e0451a2b6c26
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8b2d3e73-1846-433d-ab71-462faecb55dd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: c34e0e3c-4090-4c95-9562-5713acde7eba
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 13a6ff2d-ac7a-4bb9-8b1c-616abbaccfcf
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: a10d7cfa-6afe-4b2d-9508-a807aff1c795
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: c15b8a9c-95cf-4f8c-b465-c016a70cf921
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 747e8f36-e4a7-4e4a-ab26-31ae361778b7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: a51f4579-5665-4e4b-aa3d-4090689899bf
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 10975f00-be07-43e1-a0bb-f4d5b3714e3c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 453059ae-f584-4bba-b349-8b769b285c71
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 99bad294-abf2-4d98-aee9-a99096e7868b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: f9a0a897-0930-42e8-aff1-afd17feb7fcd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 894fa2de-96d5-445e-a955-ee78d4fcf313
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 5206f4c7-5fd5-4018-b3b9-bc6ae91e0d23
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: aa65ea48-43da-45bc-9eda-684d77a1a383
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: fb49a22c-9b57-40d5-81fd-2cbef87c4731
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1ecd5a1c-50a2-4a2a-8211-b3a190b684b8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 020ac222-8550-40f6-9d2f-618b28c73537
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 26ed32ff-a507-413c-afd4-15f4bd86fb93
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 08ab775b-c4fb-4fb8-a11b-cae16c2ec225
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 64536465-5b6f-45eb-a98c-652b7691a7e8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 273e1a8d-f594-44bb-8f84-016294145284
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 28d2fcac-d68a-461b-aa42-52f5909e1c5e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 0408eede-a097-4b6c-9ada-3e65045e793c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 793dc5ed-4c08-4e00-a45f-c4a7bd34fbe0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: b1f9d15a-ee51-4b0e-9e9f-6413936b9ef0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: ba6fe7a0-eebb-483a-a659-9c8e85e273a7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: bbb5cc28-8ebc-42b8-9706-487215b8f14c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 6b8e7162-574d-40a4-a306-eca96a1917c8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 3c4bd7eb-adf5-4909-aa75-ad5b98c54f98
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 83e756bd-01c1-4c95-af68-d2f7cbf281e3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 7334f628-5541-4359-a47b-b73115f6cd7b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: d92e9041-657c-4b5c-a773-bdb6edb0d009
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: a279e26a-8c57-4536-9dd0-0ea197e67873
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 01554e2e-2f09-43c3-9a31-8c070b4a24a7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8e053526-98df-40fd-be0c-bac732e25979
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 0e9217ca-d5a8-46be-bba0-25a9fb3d82bc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 2253611f-23b2-4c51-a9ae-ddf5009a95bc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8931aa0a-bd4c-45f4-a26b-c4cb8875ae3a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 30980304-d12f-4f1f-b993-43e93a28a45f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: b5be33e8-0244-454a-bda4-b616ca515ea3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: aa8e4f41-07f6-41a8-8000-b2fcd8ac5716
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: cbad4d37-e758-4115-ab51-60e4b51b7277
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 4aebf866-b8dd-446e-8496-6ff89b8ec70a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 5236bee9-bd01-4e42-b28d-5b9a03ab2bfc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: ca8f5f57-c70c-40d2-9902-bc3e9e8d22e2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 30658be3-5613-45ca-930f-fe13d7986d43
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 6735a773-64f8-4ce4-9da7-1b5efcef9895
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8569bddc-d0ff-4d7c-bb95-360652fa7f72
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: f7a8c54a-a845-444b-8724-a2481fe5acd6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 05a32f6d-07ee-4bec-a750-4522c8835263
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: daba05ac-92a3-45ab-ad6b-c3d2cc0d8c41
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: cb707081-6c81-4f8b-8557-c5bee8aa5bed
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 48f1f6a6-1c00-4073-b8b5-58d55d37d473
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: dd800ef9-219b-4d48-8267-6f7a31c5c65c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: dba8b5f5-66c7-4fa5-a635-a1ce274d691b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 7e66ff54-6a3c-4c4b-b50a-aa16efd246aa
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 80c88cbb-1119-4e6f-99a2-a1c9425c3b10
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: fc76c440-d568-406b-bc14-9dcc53b55c7e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: e456b20a-c2f6-4807-bbb2-368f075351d0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: bb1cd12d-2954-4041-8546-3da386542608
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: d9ff553b-b0a3-40f4-b7b7-0cc5fd24158b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 47d6bc2c-f9a2-4711-89d6-ff1cd7b79f30
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 081b150e-350e-4844-9369-de1b8b4c2030
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 9801aea2-93c4-48af-988a-c14172d49cc7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 27ffcecb-784d-4053-ab29-6680e3fb5364
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1a79e4ad-8398-4ae3-865e-f5146e8a1aa2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8c6e6433-6a92-4c8c-b6ba-4d12a7df13a8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: a953db03-e8d5-438f-919b-44de185c58e7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 7fa7b458-f07d-4583-8449-ab12bd935f09
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1d8703b6-c3a4-43bc-b345-fb4892149742
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 4ae49164-2823-4e0e-b5bf-8a09b0baa2eb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1464cf55-2988-449c-b13b-a5b35c1a1bf9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 5f78c8c3-6707-4348-9640-928d9105a4d7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 2dc3deb3-88e9-4550-a751-b49326910f49
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: dde81c3d-3b79-4cfb-9e7a-3fc3bb7fad84
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8808dcf0-ff50-45fc-8fec-0a3d29f793f6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 9abbe7fa-672a-4444-8587-18192d151252
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 335ac549-ce61-4eec-aae3-d5ade284c004
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: ca4cb469-609e-404a-8403-4c1f59eeea78
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1a7f8487-b35c-4734-9ad2-946e0e48da2f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 26d0b084-acc1-49e2-8080-74460d5461fe
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 0369e603-31ff-4b04-babf-dbff9cc5e114
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 975a5de9-e46f-4b7e-a5a3-cfeee3322226
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 5bca8e0d-c2cc-4a8c-840e-f48075db62ba
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: fdc7c283-d59d-48ac-a8b1-52de29dd34a2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: c8619155-bafd-427b-852e-9cfb8d142793
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 68387a18-d001-4f7f-b899-cc08aa6bce03
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: fab96ae3-d010-4649-91b8-1707ecf00bef
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 116f1df5-28bf-47e2-a6c8-452f8654c5e8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: f572a2c4-2a2d-4a55-bfc5-189767e274ee
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 6339d991-7b1f-48bc-a3a7-321ac09aa359
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 56724c58-0e53-4d37-833b-72cf3bf0678c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 3afc826e-6979-4931-898f-dd6c3692e8be
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 695e3fee-9eda-4d4f-bb74-e03e9c4a3512
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 5ab91a21-31ea-4583-8c37-b3703e219b40
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: bab0d97c-4840-457c-92dc-7f2ceff5d109
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 3d50e1b7-f3d6-450a-bdaa-bba635474d53
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1192f575-424e-46bb-a6a7-1f4ae5dd923f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 52460222-cd93-41af-aa21-91417bce8725
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: fc2de15f-87fe-4cdf-8467-206ffa341485
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 2885812b-e447-456b-85f6-02049f95e92c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 057a8247-2cf9-4e29-b8f0-728a9c1ad648
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 167cca8b-5e34-4bed-992e-49e5e5ab1ec2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 8c4fba73-fb6e-4aaa-80d1-2b1ddeb13fa4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 059e1132-e5dc-4e74-9d41-74e9bddb728d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: e6de381f-5fcb-4be4-89be-b150a641f53a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: b5353b9e-cdc1-4ba0-87c0-c790e5f8d8a8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 1c7d52c2-6d59-445b-acd6-b4ce25baceef
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: d7da6684-be18-4933-b106-544414277525
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 6008e1be-1c4e-402d-a51d-00074dfab503
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 3dd28246-2510-480f-824d-fdd63ba9ec42
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: 95122f17-c380-4f88-9055-cefd5d4737d3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: f7b46005-6234-44d3-a4bd-34345de2552e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    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: e724deaa-db86-46a3-bd9c-a251bc60eae7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound20.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound20.c: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound20.c
    file_hash: d6a7b66d62d8261743d542694624b328b551f76289ee08b3039b7ca01c3c317e
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
