- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f44fabf5-97d6-4c4b-a67a-6d1ea0afd189
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7efb569f-a871-46de-ba8e-bce7f43e24de
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7936bbdb-9b2b-49ef-b4c5-80b2bfcf4152
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10a339cc-486f-4eed-8fde-ae5627c10da2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e6e3351-23a4-465e-9f72-e4b0cb47388f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8884dd72-1a90-40fd-8cbb-abc3eede7468
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dcf0d9a3-56d1-4105-96b4-be003f0baea4
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e494616-fde5-482c-98ec-14b2a5d2062f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f51878a-62f9-45cd-8b0e-391e270ffbce
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef83671b-f2d8-4cf7-8ac7-a8e6d1f420d2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63b9b8f1-8552-40db-9e28-0732ba24c159
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33df5b83-1cb4-49ca-b694-fd065c5b9678
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7633f78-994b-4b66-8ce5-8deaa8fd361d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23db125d-e571-440b-9dc3-66dfabe4fef7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23d2214a-9af6-4674-a541-a82a36fa32c9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 863d7331-a70b-486c-9c64-bd9d93f02461
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be5622dd-d348-4cec-ac41-fe9b17e6a122
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 874aaede-352d-4e91-a0d0-72d4d308bb00
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9c1b9d9-6025-4a98-9385-601b8b6009d8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a16e46a3-3d0c-4525-8ff4-aa28ea75ce7a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e57b7428-c4fa-4a3c-8162-9f5d139d5608
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0821e67-c3c5-4205-96d0-12991ee270ed
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49400145-73d6-4fae-a368-46079e592b90
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70864cec-e3f9-453e-8a1b-bb787970fef0
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfdbc558-a72b-4cde-b723-8c6a31450683
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2daa07f2-083d-4809-8a7f-b45f2aa556b3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6db89712-2380-448a-a728-b8c2f58f8f74
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 135f616b-5667-4061-bf05-c48ee7f85441
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa37730a-762e-47c6-b043-497f3c4faa9e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25521344-e771-407d-a969-5a53a61b8651
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f5f0e90-19d2-457a-9b9b-d6170e0236ac
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01ffe15a-6e02-482e-b96b-dc689251aa32
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0036fadb-7b5d-4920-8af3-921e479a40e3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4b44355-d237-412a-a3bf-ad74a31dc077
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7c73be0-1b6d-4d45-a191-e92cbdb97e2d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 897ad283-f93e-4609-b70b-fefa9a9f5829
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9fb5d8d-684b-4d9c-b098-86c1c57b72c1
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac640109-2262-48f3-8f96-ba0c616cfe06
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd91456b-8c61-4059-8981-21b3da8b7188
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 211bc8d5-2a72-4233-8116-8192fbfc1b42
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8c965fb-aead-4649-b685-c7853705af0e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (long long )A - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b8d250b-94a4-40fa-a294-152319002947
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 46
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58286bf7-6960-40bf-b7d3-27fc2ad87df8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 47
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )b) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89f7d78b-e05e-432e-8215-f512de545644
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 48
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfbbd71a-647d-4fa6-944b-0fb9243f8a52
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 48
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )b) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d50c507-3735-4a2a-84bc-5b6dd33af928
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fbcfc78-c3a4-4e0d-aeba-ab3f2067d460
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c0a6eae-f570-448f-b12c-2bc15a918cda
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2ab0a6d-4acd-4aeb-a000-1bd43494fb31
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 278aa5fc-8339-47e8-bc61-80deef808a66
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d5f8993-e649-404d-807a-fe40470cd366
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 761c44fd-fe72-4f59-90bc-fcabf36020e2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9b539aa-50a1-4d63-9058-ba37d3ab6e67
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1589f96b-74ce-4052-abc9-988b57032153
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26d2b574-8c69-499c-ad5f-c206df6f2979
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4ed432c-ee22-48a8-abcf-488986bf6e42
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3b6a387-96be-4ebb-b4a2-a5c74d393b70
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 642366e5-dfe8-4b17-aeb9-1e91dc637a54
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cecb8ad-abaa-4f41-8e7d-cc39b34bbfad
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67137b8d-d3c6-4466-9075-e912fe2c8589
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54dd961d-56ef-476a-a5ee-e9764f439e45
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0d8de4f-d48d-4179-a968-21fb165553ed
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e65ea385-b516-4dd8-bf52-bb689606fa2f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f265a08-7407-4e50-9c38-a34e8ccaf443
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bdde80f-6187-47f4-9b74-43d3d4cf6e06
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound100.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound100.i
      input_file_hashes:
        ../plain/divbin_valuebound100.i: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound100.i
    file_hash: 918183af41ed822b080517d21adc4e88771d95d1ab967de55d618cd7a5912a2d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
