- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 518870dc-73e2-4d87-93fc-357ca6fb6281
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 37
    column: 12
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53a7932b-9046-49f1-b163-8e77ddf01b64
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23caef74-5c7c-4ba9-9471-c1e08811b059
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49f4a16f-06b5-43c5-b56c-560c4ddf2740
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a496fc1-5479-4559-834f-a8338f7ef428
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 37
    column: 12
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce90f40d-eb86-4089-b688-79555c630635
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 37
    column: 12
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4c6be19-23de-4a06-9706-4207246e8d15
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3a2f364-863b-46b5-9990-23973a555866
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f6df472-3aaa-4eec-a761-9696e560936b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 173894b4-f079-4107-875e-55f04a4e114e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38236f78-dfe7-43b8-9e68-716f478a10ed
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    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: 4eb11f90-04d7-4b9b-93e7-bcf42e75bbdd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63dc57db-5605-4602-9c87-6c6ee3321288
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afdf724c-ff6f-4b07-baf8-fca719354794
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: q <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a75aebf5-73a9-4351-a4a7-000aaf75c225
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3b447ea-8c0d-450c-a540-223eedd3d973
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1debb45-0ef6-4b0a-8a68-610ec5d4747c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2b3065a-d4fd-4d9d-930a-19ae0b2b8b44
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f8094da-6293-4a94-9fe7-288dc1c1b049
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82f5d514-1a1d-474b-9361-0694dd5d2e85
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57ccef4b-4b65-44f9-9ad1-fe38f24e14fd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e748b854-942f-41a1-93f5-7e7c87ac55da
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20251d6e-e392-40d7-8ff5-b2f196d6caa2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 43
    column: 8
    function: main
  location_invariant:
    string: q <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e558a68a-0a0c-4166-9a5b-6a02ee4bc493
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e246be8-7f04-4af4-855a-904c015ee855
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56a4677e-697f-4d57-8bc1-1d57107c5903
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b3a5547-59fd-4d69-898b-872fbfd20466
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fdcf83f-57ae-4663-bbfc-90bdba53f303
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 148e2264-f91a-4c02-83ee-ab8701de77db
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a230ac4-bb39-4525-80f2-34ed1c2cb737
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a89e245-3e88-4b2a-9de1-0a8138ee8986
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b220daf-efcc-4272-983b-7e88b36c6c0d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 44
    column: 8
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b4c5f67-ce84-45ef-914e-7cd712348999
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 44
    column: 8
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 438b6985-bf8b-480f-964d-614c9367905d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 45
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e35ca1ae-982e-4bcf-9654-8518dcf74e95
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abff3937-a30e-4cba-ba16-ca67f392dc72
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08dc2fba-f261-4e97-86ff-a582f186da3b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 45
    column: 12
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2c0c094-7b0a-451c-bc7b-54acfa50a319
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 45
    column: 12
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80e9b177-a30d-43e5-b1ca-159009d0bd16
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 46
    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: 922711bd-8484-4888-acad-37904e3fbd6e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d380d3c1-18db-4ad3-9b8a-63c971b1c513
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 901ecd03-3ec2-4c5b-b984-19544fb8f279
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 46
    column: 12
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c9556be-cbfc-4538-862e-e01eb312fffe
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 46
    column: 12
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1788f41f-8f45-4e7b-a6ca-86dc8d883894
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00a52211-a93d-437b-a9f0-6e3f5e7d1567
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: a673d035-c03f-4081-8fd9-0996892fd7e3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 786e700c-24e2-4968-852f-a53c7ef68be4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ceefef3d-112f-4397-a33d-68f775a01a8b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 983abfaa-1061-49c0-b246-51e62831cbcc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ce8f195-2b02-491c-af5a-5b0fd4568da4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 50
    column: 4
    function: main
  location_invariant:
    string: q <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8bb50a1-29a7-41af-af56-75fc3eaee0cc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 50
    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: e2e76c6a-8cab-4913-bb4b-a34c4bbb6b9d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 50
    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: 6902f785-ac32-4753-92a8-fbb57e5d1ef8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 50
    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: 91795172-bbec-4a78-ba3f-0fa3f07ae774
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 50
    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: 2f134298-c904-4912-8fdb-e789d4d925bd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 50
    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: d771ee9c-912f-4d04-821c-714db8d81e3b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 51
    column: 4
    function: main
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e1888ed-7b90-4427-a003-b149e0a4c822
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 51
    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: 553b24e2-0b4f-4dd4-bfbb-5033c999d62f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 51
    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: 478ddf8d-1326-4f0b-9aea-9a401e9cc109
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 51
    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: ab32b44f-8ab2-404b-8d02-3e5b68406ebd
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 51
    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: 775dd2c8-3e44-4ba3-9823-6029af3e1579
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 51
    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: e778c180-9b95-4c54-ace8-a4fe5a1f3885
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 12
    column: 159
    function: reach_error
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19235db4-a433-4cfb-b0c6-336d4e6cbf7d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 19
    column: 8
    function: __VERIFIER_assert
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c25cff3-e756-483c-a0b4-4a7d3aae46c1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 21
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70a907c6-48cc-4af2-a952-35b2da152d93
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 23
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: -2LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f71ced37-fcb8-4e64-9065-9ad2d6178325
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 482f35f9-ee01-4ccd-8d5a-b5eedb3835ea
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 3c9119de-f451-43b7-8d9e-46a1c849c77d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 85c0b0fd-2eac-467f-ab60-842490cd4a7e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 070b74d6-38f5-4ef9-82d1-f180d2e65044
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: eff342bf-33ba-4f13-884b-0a4bbb751d98
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 9df04ec4-5b31-42e6-871f-198d14d9d74f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 739e72de-caca-413b-b8d7-a6c6b5d41761
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 4a0d8cde-354d-4fc1-93bb-852eedb25f46
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: eaa2c66c-a807-4d29-86e3-f6e59a326551
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: b1272ae2-5340-4ebc-988b-2a9cac07a365
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 30
    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: 4c61460f-f0fb-432b-8099-54da2122d7e0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 77c7919c-df50-488f-afb6-e6e2fb51b3fe
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 0ce1c242-93c4-418f-9f69-11f69ff09433
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: a6217638-3c38-4648-aa96-d1f74b537a6b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 755152ab-dbbb-4164-bf7a-f9bdb5dd43df
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 30
    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: 4a459f59-5be4-4bf9-a69e-4a1847a0a744
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 2e56b221-bd77-45f4-8b0f-15b0ad2dac71
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 4b7f994d-925c-44c3-b0b6-f7576cbbf55c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 080c94cd-1610-4d0a-854f-4abe56c439e6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 77d69218-ca7d-4a62-ad1f-2f3c3104769d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 31
    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: 2993ff62-a592-4a5b-9967-e6f326015d1b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 9840d258-359b-4d84-acf4-38bcc06ce827
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 250cf6ae-3503-4bb9-8573-5ee80b6758ac
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: ae528ea5-125e-4ecd-83fb-6da356e8da9f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 9d7e8d33-48cc-4c2a-87ad-e1f59a9d3bc2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 31
    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: b4372122-b24e-4493-9a44-770cd50c9810
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: c4e24e75-eee3-474c-a044-dd76ae86a16b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 9471f3c3-fd49-4849-9845-b03ca2666e32
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 2da76084-9e52-4a89-9bec-fa0ae019d768
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 6bb8c971-699e-47ad-9361-a87b5232cd3c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 32
    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: 50761ab2-480b-4da7-8967-fb65dee55538
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 67559933-ddb3-4d79-9e19-35736b7852f0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 19516222-18ea-4307-a4e3-1cfc044a58d6
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: d8775b4f-a7f6-437e-8d71-a83c5117984e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 1185c6cf-b9be-4f50-8d9a-c03543e3ce7f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 32
    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: 6be70ba8-0096-4b9a-bf16-8098fc459e14
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 8274d870-2869-4350-878d-82a93c0803ef
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 341b9cd5-437d-458f-9e21-91dfc7bb30d7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: d26141e0-4eac-4867-9c5d-9a2985836037
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 8d7dae59-16ae-49d3-af93-f18151c2fdb9
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 33
    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: 0c07667b-ee64-4773-931b-67b9ecf20480
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 1df6bb0f-3017-4c4b-a568-9109f565d834
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 176a65af-518c-46e6-a141-9ec3f8fa042d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 1c40d857-3386-44ea-9926-9a6f26db219e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 074f3918-0938-4058-96c0-549baeb1c3d3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 33
    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: 66bc485d-376d-46af-b7b0-6efbd6d44ad1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 71a1a1b1-07fc-4f00-a605-e50318ad4e01
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 8af4728e-1e25-4162-b3bd-9905a5991be4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: fc4f2fe6-ade2-492f-a573-1da6095aefcf
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: d08e9700-8f84-4cc0-8190-2023ac1dd65d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 34
    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: bf1bb854-65e7-42dc-809c-29e611177e68
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: d1da85ce-aaad-45d7-b952-d44f9d61ff56
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 65c71f8a-d1b8-470a-8570-8d03fa4ac84c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 6b6b2436-46ff-4f84-b260-c322b6941ed2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 34
    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: 2824b441-83b5-40cc-a3d4-7c9399f8e1a7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: fa1e12e0-97cf-4653-824f-d94d3fd2f37f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: 4f1aa60d-5325-4108-ba16-56ca73fe43e3
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: ea09e98f-e281-4be1-8caf-92e86a81999e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 35
    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: 8d4be2eb-e544-4d05-9b8f-520d15270ade
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: ba9c6f4d-1907-4873-b5b9-1c3a6a1d1186
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: e960873e-b338-4901-8114-d60a819a58f7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 35
    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: 93c31b4f-84f9-4dbc-8634-f95061f0b7a7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    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: b75ac32b-c553-4ad8-baa5-f962b3b7b4ca
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: beaa9a83-dba1-4c97-9152-0ffea9ddc0b7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fd0945be-91e1-4488-8046-084445e72ae7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3002dbfb-1f25-4d2a-8bee-830053152512
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 08a57fcc-f856-4490-8c02-125c53a8ec00
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b511fca0-1641-4064-989a-4f9ba8f7a144
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: afb10241-3d45-4912-9675-e6bf107be551
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b1650ab-90df-4d8b-a76a-f49b67360e88
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 64543156-234c-4a27-b94b-febbb02553cb
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21489e6a-b513-4bfc-be33-fb2f6f1e494a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: 1 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9d59c49-2979-468b-8b2d-50dc630218fb
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: q <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d5b9be3-d64f-4265-abbc-3ad44d075a73
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fef0534-8da4-48e0-aa8f-540c1fc49ec8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d95b1d07-a831-4033-add7-e7daafdbc14e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 468adf49-7456-4885-8511-d0409e13f1c2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5770d4ef-40f5-4a00-a7b8-254787a31b70
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound2.i
      input_file_hashes:
        ../plain/divbin_unwindbound2.i: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound2.i
    file_hash: ab65f956ab163b80526b0084797effd91e1aac547effeb9a1fdab821fa279e8e
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
