- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c55e044-a61e-49fd-a9ac-2fa3ee6a82c9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 27576db9-8dae-4e29-a4af-95201634d82f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: aacb0310-7cd9-4da6-b40c-a024044797c5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: ca590b4b-f3c2-49b4-91c7-38e6f48d1085
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: c5f445b7-326a-4353-b367-da7ec045b115
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: adab4b49-c765-4ae1-af81-39c677848035
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a5c5cea4-8751-4f4b-b46f-845e2920a8b2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 2f144fd6-1ba6-45c7-add2-b70e52ad2bc1
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 1fdbe847-1c60-4f32-8ebf-0644155b6938
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: db440209-809e-42d4-a85c-b2f278ebe44c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: fd252714-58b8-4045-8f46-51bb380e7f6b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: fe6a4eed-516a-4932-a374-959c70a45441
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a98c6d63-537d-4cdf-b336-e77885b83a59
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 5c7e0935-9028-4c92-ba28-46f9d6fe9317
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: f71a526e-ceab-4d03-a0e4-9814b4945d9a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3d2d2d89-776c-4553-96e7-78421df8988e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 89f86a51-ed8c-4c0a-9fda-f11bbed5406e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 2a3178a1-f29f-413e-8dc1-ee839db54d23
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 7c559f7d-a813-4e34-9a26-35e58894b746
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 5034e59c-9a69-4d6a-8a4f-2fd33da1700f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 655c430f-9bf0-472e-862b-5eef5c840301
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 59c02d49-85e5-4fcb-94bd-bdf61f87bf88
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 7ff9a76a-4ad5-4074-a061-229d4a9664ff
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: fdfa7b9f-84f5-4e67-b529-87bd46a7acf6
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 98a1b3a7-e5c7-440c-a8d1-5928fd336da0
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a46151b0-0291-49af-9e7e-028903c426d8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a23c13f0-d3af-4d67-ae82-697448567deb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 9df91ea8-adba-4b4e-af5f-d7ce7b93538e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: fab91920-ec47-40a2-8e0b-c4f6fed7e26d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: dc54c567-a38f-41d8-a9aa-2a4eb21b698d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: f92a971a-3c1d-4d16-8e35-f7dd0efba30c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: cefc18a8-fc41-45dd-9f2d-ef90db869e04
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 7c98d5f0-c1f8-46b1-a291-6d5ca2f02cd1
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: ede48507-44f4-450c-bb0f-ddd0a96d3f7b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3f891192-3e0f-409d-9515-cf55526baff5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 690ff481-3a8d-487f-b974-e90aa85ebe52
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 1beff7b5-2d28-40ba-9bba-1faf38bb13e7
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 5c492dc4-d0c8-4118-b37f-ab59764509c7
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 35fe9621-4690-4c49-b621-d07d0d01af30
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 0e8b111d-d1cd-48ac-a44f-b8f30db5ba17
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 04d07eae-2ca1-465e-a9e9-39f0c7eab8df
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 9920216d-4b11-4e92-876f-844a83e4afb4
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 8a4f0ac5-eb39-4787-a05b-174796a6483d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 8f7f784f-0b26-4b64-b462-365e219c7c47
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 02acea42-428b-4932-9855-6d10cb3da488
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: dcb997a0-c920-40b4-9ee6-9ceca1239c03
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 1b27a2a1-0a0c-4d11-b0a1-8a639198951a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: d3ce094e-4e49-4424-a906-314aa83f5e6a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 0dfea556-20d3-4cc6-ba6a-e5c8d15c525d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 6c3bcabe-c508-4ca1-812c-f6cd6f371252
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 82d24e1b-7db8-4600-9e92-432e6322cae2
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: ba583991-e638-42ea-b9b2-5aacae87a481
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 1f246085-72b3-4f32-a47a-906a246f1d46
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 2c6ae699-ba43-49e5-94a9-60709cd7a1e5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: e6e9ff57-09cc-4ad4-8182-09108c814319
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 6609f6ca-7d55-4bfc-841a-76a4f73375f8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: e30bba2a-9c6f-4fd6-9563-55e43367b866
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: dd098e69-6345-4a9a-8287-c34a44f342c9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 76503f73-72a9-44b5-8878-e48322d0ae8e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3744b77c-8ab9-4f74-8425-29a57bbdccf9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 1d213d8e-af08-41f8-bc35-c297f2402dde
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: d0ebe866-86ae-40d9-b90f-99317e987dda
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 19512b7b-f2f2-4c20-a84f-ca9112dd90b5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: c78ac167-7c41-4889-bedd-d5fbab324e8a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 6f334a13-0b83-4b62-a91c-0a2415bc3e08
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 9278f681-4d83-4d50-900d-c375b1aaf194
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 2e03d9e4-9e92-428c-b5ca-7ea82df606eb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 2bea5d0d-8858-4e42-96ea-03cc4300dae4
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3ee4ad7d-b470-4c16-8f7a-b66a93bdeadb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 0f06dc40-fd6a-4818-a1f5-251700a6a33a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 74cebbea-bd03-4a89-9f30-ac1998c7e50e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 54298028-28ff-4267-9a83-45e9ff03a18f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: c0804094-8987-46a9-acae-2bb848172208
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 063c5ea8-dc50-4a41-97d7-22d5fce05bf9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a06fbba9-60ef-4f13-8b92-460c26e9be1d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 5c0f8b2d-115f-4cb6-8119-75380ae24d08
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3db31f03-1c3f-4442-9acb-c6efe1560c2d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 21127851-c812-4bbe-b8f2-7d21b13bf8ea
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: d679acda-0899-41dd-bc73-8b81f22b8d2d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 5fecc381-f0ce-40b9-9a56-07bf6ae0c9d8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 62ff78ec-6c26-4bb1-8155-152d92ecbc60
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3dec7d4b-cd8e-40b3-8c41-0bd5b13c2f19
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 8d316966-db1e-4c6d-8e9f-8440cbcaa371
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: cdad5fa8-9bff-4010-8777-3e5e3b9559b9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: fc269583-56fd-4124-88e0-bbb5706cc9eb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 3e9dcc05-4db3-4b97-9c82-15d17cf06f88
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 10e8ac9d-10d8-43a2-bc86-9bdd5ff7859a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: dd133256-08bd-489a-9b98-559f2362dade
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 532bf9e9-f97b-4f08-b4ce-9cab50c038b6
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 68eb518f-b6f8-466b-ad0f-8b9b696ae368
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 9ba51585-1764-4537-8cad-04e34a9c7749
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 42eb412f-0af3-4db6-9ca2-c8d6140285dd
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 9674205b-b53b-4e52-af52-e37438d80579
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 0ccc3e55-ef50-46c0-b7a7-41de63205a95
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a18cbb03-c7f8-49fc-b670-ba520932eb09
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 36dd9603-424f-4baf-8f96-b42980f76f55
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 0a0673a3-f2c8-4a1e-b19a-79072af543d3
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 8d313bce-fb19-46eb-aa90-8e7e02c063af
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 5df134d8-7cdd-4bf2-a94d-91e875453e17
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 64a4710a-c6ba-4567-babd-ed6df8011a1a
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: be80592d-43b4-4d80-b7d6-8392da245172
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 77af27c5-f4fa-4234-97ef-5396e15089c9
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: ca407543-1066-4a5b-a795-91f5ae7b9607
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: e2475fe9-e676-4a13-854e-fd5cc966977b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 827b16b3-e085-45b3-b324-1fbeb1b1400b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: f8a3ef6b-6b6a-4cf1-8c36-75c4c61f5802
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 4af7b8c4-c2a8-49d5-8dd9-68ab567bf62f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 6d784b1d-a2f0-4acb-948e-74341949edb4
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 1cfbc08f-3c8f-4e41-84a1-f4d897515f5e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: e8f82ca7-c43c-47cf-b434-08fcc34284e0
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 0420aa82-41d1-4f2d-a09e-73221d21cacb
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: f18ba62b-e7a3-4106-9342-ee8c119a1e39
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: c7b13b1e-ecb3-4d03-80b2-fc6fbbb93b20
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: c470cdbb-88b1-4e65-a237-82b73df0b820
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: ecfcee08-e237-4aa0-a48a-8c886a5b6f13
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: fed96989-d9b2-4951-aae9-5b87e6b940cf
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 6d848a69-8b14-4079-9c78-46f564937d1f
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 21c38cc1-4e4f-40fe-afc0-0cbb98696e41
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 8db143c7-532c-41df-b27a-282acb455c70
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: 461bc244-ad5c-4ffe-a329-a634cfd3139c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    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: a2196ea8-c12b-44dd-ae16-40984ecf1d4b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound100.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound100.c: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound100.c
    file_hash: 2b1a58ad3e10b615d95cc8c02ce2afb54c727e6977a5f6eabd49347a082a7a12
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
