- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eaf2b9a9-b918-4ba0-9464-73e5526325c5
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: bd2e9e7b-f6ee-40fb-af0a-058c2e2234da
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 4af44ed8-7677-41b1-bb72-84dc8bb7a849
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 0e6cbf5b-31c2-416a-bd27-caadf1c19464
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: b5e608f9-394c-4e9a-a131-7d16f5cb96d6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 9a4efac8-c775-4cb7-adec-84cb7e64c718
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: c730e8b8-b058-4ae4-9256-7c6a18deafef
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 36931262-29c1-487c-8937-67357fb85c3a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: db0ac2f6-3a62-4e9b-bcce-ec98f7310983
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: bc3ee9fe-a88f-4bb8-aef1-feaf8905e392
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 365b7a20-1c81-4d2b-82d6-e1e243a82e09
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 85c9403e-0813-4872-b02c-e9a63fe8fc43
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 7f475632-27d7-4aa4-89bb-5d73859e8df2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: fbe3e50e-0a8a-470e-849c-4559c31ee9c8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 6ba6d226-3c84-466a-bc62-2c59c0ae1b5c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: ac6915a2-7835-4888-adda-0cd3e6ca4860
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 67e1f3fc-22f0-4ac1-ab08-06075546a45c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: f1391c3a-7a99-442b-aa5f-8fd244c75b2f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 39d79de5-7017-40aa-b45e-3edd3a16b3bf
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 4efd73e4-1e48-4193-94d8-769d93776646
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 91072566-4f62-48d5-852d-831aec313d53
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 3cb718ea-8596-41cc-ab4e-17821eb501f0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: d829cd99-e906-4466-bb4f-d96848eefe98
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 18a4b618-61f3-44da-8d35-f7aae42d6137
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 5513653e-e127-45f1-a40c-5d09225dbd03
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 2866847b-39f8-4f58-bd81-74de9825b2ef
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 1cb04047-805a-4404-b52a-6fac144e614c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 9f349c35-da08-47be-9c8e-9ceba35d3c7b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: f5291b10-a466-4dd7-8e48-963794a0af77
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 2d706f0d-15ce-43c8-a9bf-31a6700d65a4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: b334ed39-32ad-4cd7-99b9-9e75a0d47568
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 4c0b778a-b5e6-4652-9567-7b5f6da602ec
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: eca62e0e-36d7-4920-8fcf-71904824b104
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 3d768b2a-1ea3-43b0-9229-e23cd78ae53c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 4d1fccf7-8a0e-49ec-9bd9-5d822dc49bcb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: f78ad269-5197-4bf0-9821-2bd1e18e4d74
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 940a642f-6ee5-447f-bab3-219952c42f90
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 8d18c9a1-8bd1-45a8-8cdf-55fd7bc9ccb9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 82206a2a-8137-43be-96c4-730573cfc1c3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: b02e6853-1af2-4ffa-b266-39e6bd82f84e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 1bad9e61-349a-41d3-b24a-40aa4a6bf1d1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 4c00071e-bd7f-4e44-950b-366ec2ff504a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: a17fd615-c04a-4a87-aad5-60c220c8ad3e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 1137199f-4ea0-46c8-a55a-4341287aba80
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: f82ff0bd-3e0d-40e3-86aa-19f79bfefcaf
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 1ce305a3-b976-4634-8bf4-4f8494fd8289
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: dfd9ca8f-fe35-475d-b956-c5982ccf08bf
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 76dc0771-6eec-4780-9870-a1d45dfaaa52
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: d362e04c-0ba8-4dc3-869f-a076512a87da
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 415ffc44-b850-4654-ad13-14d8cd1218ec
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 60af7e3c-4ae2-44a0-82a5-46cf689cd7ea
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 125d9d8d-17a0-4c6d-a804-b7e03ebb6666
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: c789a3f0-964a-41dd-ac09-6cd618c5e776
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: b23ea17e-9c52-4403-9244-4d5b9169869c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: ba890367-b180-4126-9266-eb11c81a1bd2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 690a1df6-9d09-4c24-bc63-6a3baf12cc7d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 29cfb918-69f5-416d-b03e-32253a4462f2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: adc4c196-5bd3-43ce-b66d-65023186f1fd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: d942a929-f88f-4e7c-8907-eca46766766b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: c5d9c60c-4a49-483e-8a3c-f3749577e06b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: dafb8819-4254-4fa9-9ec4-94f633fe2fb4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 9081bf97-54ff-4e97-be43-50e6cb061a9a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: d0daaebc-e659-4491-8a6d-ac587ded98a0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 3e7cdc95-5b0c-4661-b065-3f90862aeda7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: a83c2755-dffb-4833-b03c-ddda98553904
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 2cf5b244-8b47-463b-8bb0-3440040e9167
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 5476b3c2-9992-4f53-8ba5-bee573a7d3b1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 69838898-eab4-4a0c-8f93-31bd7d9463be
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: d95ecb67-3682-4291-9a54-bf919e324c7b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 5be38e64-746c-440d-9f63-f80fcda5f9f1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: cc8133b8-8670-4d90-831b-ef97d154c204
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 0c007c4a-3707-47ea-844f-dc22e43276b8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 1de977ec-cab2-494a-8ddd-e23d71c5ef0d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: aa8cbe17-6ae2-4e2c-a558-6167101f3d1e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 873a1c77-bad7-4ae0-829b-c130dbe97346
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: eeb79aa4-c28a-4e8f-85b0-49ddfb4d33d1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 20e78c23-0d7b-49f6-9836-a5e81ffd1d39
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 137b9fd1-990e-4fa0-b2dc-c5ddc383f295
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: da3b65b2-d32c-42f7-b85d-e4095b77a52f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: ca6c7c18-c340-47b3-99be-a1c2f693ac8b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 860109f5-ae88-4179-ba1d-d0ed686727cd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 38c8d2ac-3e0b-4535-a2de-792d829ead00
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 3ed11479-1e94-4c0b-be5d-572b1bd84fd8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 2b22850b-4652-4a1d-ac77-f1cc4d8bc6d1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 922201e2-a547-4df0-a72b-8e636e033079
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 266a2144-2754-4cf9-aa5e-02df998b273d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: a9432d31-c493-4982-a65f-d240191e203a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 61b45077-d54d-4aa6-8d75-b027fe764abb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: b87bd91c-6b23-4f32-8ffb-59d020db13b1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 14143fde-f5b1-4af6-93a3-361dd268847d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 883eb19d-e541-41a1-9664-e9c822221bfa
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: bb7afa0b-19aa-49a8-a744-24e7c7690b67
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 5f05065f-8238-4655-9ca2-0da8e170e019
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 560b15d8-d2e4-498b-b832-a5ce90886ad6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 89dd30be-c12b-4627-9ce2-14f948e5a9f2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: aad31b10-ba86-44c1-9221-4061123a504b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: a6e7b1da-6505-4c89-9b44-4477fe74fe5f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: bc3dc3e8-3e8e-4c9c-9078-7c005e420b02
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 721ba0c9-da53-4dff-93f7-e881a084ee9c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 9d953161-7638-470d-b9ce-3e525380db41
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 89ea8f54-d3e2-4bbd-b965-6229b47d85c6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 3831c12f-b95d-48ba-ab1e-70874462680c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: fac554c5-005c-4395-a3aa-29880cae9565
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 4c655b18-c0fb-4043-b8e1-9b535aede577
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 650d7f3e-ee84-4260-950d-f9c38871f376
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 777a4d4a-575d-4d8a-a358-4df816241046
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 8415bfa3-a416-4c1c-bef5-222d789c7cff
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 2fae27fc-96c6-49b3-93fd-a11c1de568a4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 214a93e0-04e3-4659-9379-d8a0086c9f0e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 03816413-40af-4e0e-a4b8-e4db812038f7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 7b0dccc7-83b7-484f-9bbc-c3a6607995ca
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 7d6165b8-4d30-44eb-b6bc-bfae0ccb96dd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 367751b7-ce1c-4252-87c3-86ac39859384
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 6bc52cf3-ae83-4480-9c41-f0410a50bb82
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: c4091331-0a8f-483f-bfe6-7eadd3c59480
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 0c1c9732-6fe9-407d-944d-a8e54056bdf8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: b37157cf-6429-4762-bcdc-0446d3e7c1a6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: 1de0d32a-067c-47bb-8242-530e355c1b0c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: bd8bc116-0e18-4e71-a5cc-be68e06b2ade
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: c5ceff4e-ca0f-4443-a828-5c3d4a5cdd18
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    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: bf030ed0-49c2-4c4d-9dc2-730c689fd8ca
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound10.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound10.c: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound10.c
    file_hash: 879a640f466eee273c1bfb9ec38819f0b05c8e28dd65a68aba774d943b257ad3
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
