- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50ec36db-4224-4fc8-a729-482e743e860f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: d4ee5826-fcf1-4b2d-b525-625a6554e994
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: b41c6e4a-8fae-454e-9a47-e3bd1a31c5a7
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 1d48ae5c-80f5-4e21-a6c8-de19057ab71c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c7d37c1d-fbe5-49f8-93a5-73d5353d6747
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: ff3f7775-bc30-4f71-aba2-8293c72c302e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: f7a1dfde-ea6e-4568-aa66-d7e408fa7eaf
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: b63ffd5a-08e7-4db4-b94f-83943ec18255
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c312b023-8423-4306-a3bd-b60f8cf5ffe4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 63d84a4a-d22c-4fa0-ab6a-a29c9ffefdf6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: ce9784ba-71ab-4aa2-9e3c-3a590551a1eb
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: b5333cc3-829b-4750-a6e6-78a416c117d7
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: f01c4b1a-9ed1-4a15-9a10-d1adcb2bdb9d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 2acc2b06-cfab-419d-884f-ca6a6ab45ce6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 969db306-93a5-4d55-aa4c-0219c230b8a8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: ddb8857c-d330-4a3b-9278-a074a0df17e7
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: e036d438-54b5-431e-a614-2e3604679533
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 998d6f81-1eab-4a40-a2e9-723cef720dc6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c216cf3c-2532-41c2-a4ed-54a54e923f21
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: afb04d4c-504f-431d-958c-62aadbbf634f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: d7be41eb-6fe0-42bb-99fd-47e2eb0001b9
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 94403084-2a31-4b29-9810-6b977df1318c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c61a40b8-b96f-4b7b-8a3a-2ed42aef54db
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 86508ea8-2b41-4299-b52e-7cf9b49e188d
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4792aae0-e57a-41d5-b974-fc2f5809f234
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: cebee4bf-43f3-4b8c-8d9c-51224e936384
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 40084338-9272-4d1d-85e8-801d9e27fbd2
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: f2ef61bd-94e5-4a91-a13e-5f4914d21eb1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c319df52-39eb-4c09-bda3-e29b29a1dbf0
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 19f207aa-75c0-4878-a619-964d7d0e34d6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c83d5ea4-e2f9-47f7-9671-dd8250bc9ca7
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: d0f3cac0-2ec5-4f76-8541-3b7188523507
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: eac49bd9-3274-485d-a5a2-ddb665723f2a
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: caed44a7-a9d1-433b-95cf-1362694e9def
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: b301c36c-4520-40d5-a267-67055881b7b6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 388318f9-d782-4173-92ea-bcad719f3eb2
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 0495b472-8151-422e-a57f-4b1cc070edd4
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: eaaf090e-863d-47df-b516-4694df625f5b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 2bf782a2-5981-435a-b971-d3a8b6afd416
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 1c44760e-2730-4abe-a14c-b4d5f8b42d5a
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: aee11259-7783-41d7-a65e-b616e575432e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 82f40fe7-6512-4df5-a849-60f93a794119
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 1aa662db-c379-41e6-b7c2-8caa079e48c7
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: e399c3bf-e27d-465d-8d28-1b867cb8bd09
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 33499ce1-a054-4fd3-9828-95ceda2147a6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 7b186a88-8996-4bd2-8c8e-97bfa43587af
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 5fddd49f-b995-46d3-9461-4077d0554797
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4fc305ed-7561-4323-92e5-5d030ad1d90f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 3ec96f37-2ca0-40a0-b6da-bf78a2ef0663
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 7ebe1486-f344-4605-8054-511adfca4b93
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c64d704e-70cc-4d8f-81ed-08b1214af934
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: eb87cdd4-8fed-4d4c-92e8-4cdd730d0bd3
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 11a47650-43e7-4f80-8e03-f6c79cb9cbe9
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4d3d702a-877f-41ea-ba38-eecdecfb47d1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c3a964fa-abed-4f92-ad54-bb2d577819ac
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 38ac916c-5f69-4365-ae1c-dae22e736a85
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c8abc963-d706-4122-baff-6339923e47d1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4712b377-4163-4bad-a2f1-2dc3b8a2270b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 62968cfd-19d8-467a-a228-45850dc78aac
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: fdb22b74-6910-45e5-a861-3f63dbddd24f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: bb8f7750-9da9-4eff-a0ff-3e93338683ea
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: edf95990-1c5e-48fb-b44c-720e3e24c563
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 530d539a-3bb7-45a8-a3bf-53fb72714865
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4f75279e-559a-47fe-ba44-597d8ee7a0a2
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 6e488b94-1d0c-4bf4-b152-c63e1541d9de
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 5156bff2-5e19-46f8-a2bd-cb0fb9b76a87
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 0ffc8230-efe0-4dc2-8db9-83f02eb20cb9
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4e96a158-d160-44cf-b21b-c22adfb05c0f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 117604b5-4eb6-4756-b72d-e57278f6317e
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c6fb5135-8fff-4c09-897e-df895220153b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 9e558adc-b19b-4c85-937f-4b702ea41c65
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 7f6ea1b0-f368-4ce1-865e-5879f15196a3
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 6681219b-18e1-4c11-a23c-53c3f7a7bb92
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 51c65ede-d158-4711-9791-b4c98e337c44
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: a884fc9e-cb9e-4b98-9293-0fcbbbcc121b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: a6c61747-195e-4a21-aee2-c52d93206131
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 5c91017f-b4a3-4cc5-8f6f-67993803e4b5
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 3961b5a5-5d82-4b74-99ad-ecd48d0a83aa
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: dc3931a8-5282-4471-8f34-a34b1b040707
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c608080f-1515-412b-9fff-3d7a09abec0c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4d40c8d3-13fc-44ab-a549-7e1ae62fd9f6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: af70df70-78b3-49d3-ad98-a989106a48f8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c29feb12-856a-4161-b213-fc4261b92fdc
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 5a378dce-7996-40a5-8d99-d549a5947d20
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: d070bca9-0b8a-49c2-ace3-3644c3d6c25f
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: ba8b7959-d4a6-43a0-a3a8-24faba0a8324
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 94d3d797-5926-4009-a3f6-c1dddc9e8617
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 27881018-2583-4a32-99e8-1a6fd1ac7bc6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 68590872-fd6d-438a-8b32-5734a106cb0b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 0416c4fc-890f-4244-a0ae-39efb4d951ac
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 472916d7-85d1-4fcd-980a-c83fede125d0
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 11a04283-9f75-4b12-991e-25ae8e54d3b1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 3495df08-4c8b-415c-8df2-cf8f062c2cd5
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4fb76531-0d7b-4790-9d38-7f7b49d499ad
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: d7fd622e-d39e-4215-9197-43d4d7eb98c1
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: a27cd3b9-214e-46d0-8e6d-468a7110bd14
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 02388b87-fdbc-4d88-822e-f6bbc5d2bf11
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: b4a36e98-f968-4f9b-af95-37e1fac335a6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 073a2a41-ba62-4e46-9a34-a6d0c37c0ccd
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 952efac2-b4d3-4ec0-a23f-d2c4d9855855
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: a3c303c4-8772-4c82-b281-d8fc4b1d1784
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: daea2a7a-02a5-4b7a-af2c-16f25a28b441
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: dbb49688-d700-47a5-961b-e230bd4a8177
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: f4a6c1bc-eff9-48f2-8deb-38299c6316d0
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 775d3441-47a5-47df-8bf2-e1a97d7a6871
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: e6ca64bc-0199-47df-b04b-179c17be459b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 17d2be55-e551-459b-8af5-b81af3e8a460
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 36bc8873-e8e7-4a03-9e31-9b35f2e8b16c
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 73e51562-aeff-4814-b66d-38a416a66263
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 90b1164a-6124-4307-b324-a0c4afb52d69
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: a5feaf44-1208-4a12-8a87-77aacc67ffd2
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 1435c0c0-52d7-4657-ba83-71cc9734a89b
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 0986c58e-d463-45c2-a411-689150e1d034
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 831508c1-9389-4921-9104-ca3aeee5c969
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: a713cc23-d50f-4556-969a-3844099cb2e6
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: c4c04de2-f8bb-4324-bf54-06b3a11a2f21
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 2034ca64-0049-4d0b-ba5e-1f989e35f767
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 1aa52463-1a12-4c5e-b148-9068765a6ef8
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: d7574477-6ead-499a-9305-ffef035145bd
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 4d1aa6e9-c307-4fd0-af00-c2cf1a70a751
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    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: 571becfa-74f0-4141-a8f9-af234aee7072
    creation_time: 2023-01-27T16:29:47Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound50.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound50.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound50.c: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound50.c
    file_hash: 3b27cf24a9b45c76034fb9a60cae976f5ca5dfa5338fef373d189f4ae84c7ed4
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
