- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 651bb865-4720-4187-b300-0e9bfd8269ff
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 9725ede0-ceb2-40f5-aa5c-1cef3a74fa6c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 40e3add6-ee4d-42f6-bbfb-4f818e9c6180
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 417e607a-d4c6-49c6-81df-6360daf87ff6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: ccdafce2-ca5a-48c9-bce7-eb08482a9dbe
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 823b4ccd-9a48-446e-be4a-c429e22d6d6f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 7814abbf-a4ba-431c-b09c-9245cf975614
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: cdc839dc-3860-48ab-942b-c3cce332934c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: cd6015f0-1d3b-4510-94cf-3c03d7b88e38
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 5234a909-a20a-451f-947c-363aa5eb91f6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: aa1fa55b-f6f1-4560-8010-faf94346f2e7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 19da4de7-826c-496b-b79b-560948479ce1
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: fb941360-e35d-449f-ad01-d717d706423c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 9ff7a49c-b787-4bc7-b334-b039ba5f4b64
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: efca664b-35dc-4bb6-b6fd-9e81a9357dcd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 59135a50-ff03-40e0-9189-f631c460c963
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 1f328c79-baed-40cc-9440-b69df22775b3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 6bfc15d7-7e08-4ceb-891e-ffc96aee605c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 65aab9bb-cd73-4e01-a90f-2160e5099723
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 069d0789-15e0-4cb6-8f86-c4d30b69d0f2
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: a49837f2-6c71-4660-b0b1-12dda28a09a0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 39eda5aa-094c-48b0-900f-fecfcd3c27ac
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: de3dcf0a-b5f8-44e9-a855-44d588fd2fd4
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 654880d5-df73-4060-8980-df06f60509a7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: f453e3e6-6141-4199-8202-2421c980a749
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 96ee734c-d2e3-4336-8313-7f5330fa3bd9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 280617fc-973b-40da-88f6-67957573b606
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 23d2019a-a793-4870-ad4a-023902264181
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 94a8e1b7-bcd7-44f9-aed3-f7c7c03237e5
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: a67e6121-16f4-43ea-89ee-94c465e98e19
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 1344e883-69c3-4897-b1e8-05730e8de4bb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 63e2cf7f-5be5-46c4-a383-f6fbb5096fd0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 6dc60fce-0f63-41b4-91a7-39aac4a4c421
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 7844db3b-87fa-4b97-b0fd-d74fd3ff66d6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b8c92959-8855-4d1b-9e3d-b710cafdda67
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 30391f9c-e0a2-4cb9-b618-1819b8157baf
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 14088768-16cc-40ba-ac7c-42e7180097e7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 20c2545f-7a0b-425d-9f52-4d4df969babc
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: a7a2710b-6ea3-4e34-ae5a-65d8a95ff145
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 5eca2035-01b3-4f29-8a5b-f263be0a8ab8
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 19552ff0-df1d-4747-8677-eae8a2a0afe3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: efabfbc7-a2e2-4d2b-bdc9-a83227a5fe73
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: e6915188-636c-493d-a49a-c29b324c5de9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: fdad06ee-d1b7-4d1b-a322-450617f20d1b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 3701f1dd-296c-469a-8f6b-7b832d655180
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 920f78a5-5276-4349-be3e-6a4125f03f26
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b4f15ab3-35d2-4792-9df8-35512f004952
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: c4eb9757-c2c7-4973-8a1f-2526e2a8d00e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 3436a83c-0c5d-48da-b8b5-b980932c54ef
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 0f8ce101-1caa-4811-9c2c-1df8cba4015d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 5ae5c971-02a4-4109-9185-5e012a860ae6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 5dd55c75-ef95-4ee9-aac9-6039e10af608
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 22d2197d-943d-4ee8-b5fe-7ac91fdb3ba3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 2ee47348-4f04-4086-be5c-8afe517171cb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b8bca22c-0860-4346-bb2e-a2eeccab9fae
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 93f052ed-b54d-4d9e-9887-25ac59824c4c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 926cb80e-3840-4fc7-b040-0e58aa4e3650
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: c6d7fb05-0b2f-4e11-8be8-cb30f9609333
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: d5f4987d-94e1-46f3-b8b3-6225e123a82e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 79d9fb5e-f0d0-440e-8805-be06f0b63e41
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 7557fabd-d84c-424b-9f34-7d35fa460a2a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: fe939ffc-f2f6-4bee-ae3a-aca8b1abbb3f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 92212ff4-5b4e-400a-9902-a1e8211956b3
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 6a22be30-6c39-4af7-a309-aaee07a7609c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: cb17a115-449d-4716-85f1-6bde05d485ac
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 64eb19a6-e15b-4fb9-801e-73efd169929e
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: cc312658-0d48-474f-aa60-72f58dff8546
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 9c96a417-ccdf-41db-9c33-053de5facb01
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 86171fa4-2c5e-4e08-bc44-1a45fb018055
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 2ca8e8e8-b69f-4f1f-8220-9c2aebcd9a36
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: cc75b027-0872-471f-a049-5b2fe1221547
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: ee033718-c466-44ea-8e15-d9d918baf5fb
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 79322cb5-241d-4a51-8548-f40e121eaccd
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 0f684888-f2f2-4a1d-bbce-80d3551e8698
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 31240ebb-8358-4e8a-8236-08fc4bc1bb97
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 4a6de74a-ec85-4efc-a5a7-0bee2570ac97
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 0722387d-570c-49e0-8726-e51b1bc5b07f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: e078cd41-117f-4072-8e24-d9caa3d8705f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 8692fa80-fe0b-4b8a-9658-22842defd413
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 48e541ba-94a6-429e-8736-0d7ac9826eab
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b5403318-dbad-43d9-80a3-f4b721d68082
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 7b0d676e-7559-4059-be35-e129892efc6c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 969b4111-e69e-436a-976d-e5ac3f9f1017
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 25b2db88-9dea-4f94-a659-737536f77871
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 75c71b13-85ed-4580-b6cc-8c57ae400cc6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: ff377cec-689a-4645-b4cb-ae8282ce2e61
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: c4184cfa-2cb9-4106-b883-b9d6c9645ab9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 80a417f4-6473-4151-889c-3e7150a6ce08
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: dee5e4e7-acc0-4886-820a-784111be239f
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 9ba915c2-b0e7-4f09-96f6-0c298762434a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: cc563d18-5cc2-45b0-acbb-faec950fce59
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b0066d10-132a-4dc5-b70c-8f04ed841805
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 956ea032-8ea5-4b40-8062-9a420ce8c936
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: dc542288-8ab6-4055-99d2-5806dcdd8567
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: f5bab975-83cf-436e-af06-34e7406fa882
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 87668e9c-2e03-495d-b67d-7467a44d3c4d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 2e82e1c3-bfd7-4d77-8a27-71493ec917f7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 9f72f1aa-3326-442a-b596-e38ad6f346a6
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b6a9c589-d313-4587-b32a-e4b2b2400615
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 981c61bf-01e3-410f-b395-2e9de316297b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 0f11d7d2-6ba1-4a77-b979-dc9b8d96338b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 7fd9f699-c250-4a42-b5ea-fd5a138433fe
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: dd53093c-950b-45a1-a5cc-667e14f65343
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: ab65e9c6-0097-4bea-a495-c07da2cb550d
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 16fb8746-347c-43e2-9ea5-6ca206c2341a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: fecf7ffc-9f30-4d38-9108-1701d69d3d66
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: bee1dea7-3fda-4a18-91e9-15ea1d2ad3da
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 600db654-99ce-460b-84ea-c19d28c75a0a
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: bb70e495-872f-4f6c-ba2b-ef26a35adbba
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: faec3c36-39fd-4664-8f2b-7b9b480197b7
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: e129d1c5-fc6a-425c-86c9-aa6d8983d981
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 4b2bd9dd-3b21-4e67-8719-0dbf95ad3861
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: b83fc742-a42f-4bff-b029-d86efc990f1c
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 9b2e3c9e-a2c1-4607-9c66-3581feb7f36b
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 0d70b686-717b-488d-b31d-f0ddcdba6db0
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: f9b5e349-21b9-4023-95df-6919323dda62
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 8e8711db-c901-4bf5-8304-826a9f4890ef
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: 8763f105-6bb3-42ed-bf24-376237379270
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: a06e2807-d995-4d4b-9f8e-f18f529fc706
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: c48c012d-b66b-4b0f-91ce-b02b099060b9
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    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: df587b3a-a9b3-40e9-879c-f61a66f17c85
    creation_time: 2023-01-27T16:29:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/prod4br-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/prod4br-ll_valuebound1.c
      input_file_hashes:
        ../plain/prod4br-ll_valuebound1.c: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prod4br-ll_valuebound1.c
    file_hash: c7f1683dc0c60d20b83300f79a9b15e37cd1fd05703e492aec10298f1b5a1afa
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + p >= 0LL
    type: assertion
    format: C
