- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d70603a-bf35-48ec-aa0b-05ba8e70e660
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: f8e7d2f3-5263-4737-9baa-6207bfa72fae
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 15102881-4076-4598-b3b6-098a3263b220
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 24164f74-1882-46b7-bba0-abda5e92e5a2
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 5996cb40-10da-4627-94ad-d0279a064392
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 94b298b9-5ca1-4764-90c5-59466b401ea2
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: db7f6f6d-d7e9-45ee-b75c-5729525c4524
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 704cc2f6-7f2c-4494-ac85-b19119a06b20
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 7d530ea1-3154-4638-8f71-4fb52762324a
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 0abb0d34-2f63-4301-aa0c-8356a4cfbdc9
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      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: 1eebfc70-a428-41d3-91ac-df5f45a94eec
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      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: 4a0227d2-71ce-42b2-8168-a60954ca27cc
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    line: 50
    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: 008a67bb-d2d2-48a7-a181-4c0c1cff5a00
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 5134490b-8d38-4077-b736-3630b814473a
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: a0361bec-6b90-464b-91d2-ff0ed0e1aaca
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 81e01e65-cbe7-4061-b8dc-332da689a636
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 4e7c0cd0-479e-4edc-8169-822418207ce7
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 116c25b9-d910-42c7-8ace-25e0ba026778
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 941847f4-0994-403d-8558-84299bec863c
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: c7539efb-659d-404a-bffe-871c5e986902
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 5ef53ac5-657e-4900-8178-13a276cfb999
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: c7b5d8e9-8447-4640-8278-c7b821dd8492
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: ea38bd29-eeda-4a82-a0b0-44eabd4c5de4
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 9a71a5c8-3ef8-4d70-835b-5de0ea243fbb
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: abac34a7-a57f-4860-b740-ca7a109988d5
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 2973e6ae-bf2e-423e-9238-9d64ce69c628
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: ece286db-c022-4c42-a142-b22d1e9d54ad
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 0b1662a6-fd76-47c5-b7ee-c96490e72809
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 87fe6492-12ce-47eb-95bc-006a6b474f36
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: e5fceb8e-7b39-4607-8397-7c9df6496127
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 110f31a6-12d2-40fc-a8a3-07709e62eb12
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: d3ca54fa-d864-4eae-8337-42e6ae6c1668
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 89de4cde-67ce-4c1c-9e39-eafe638fcbb0
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 3ce62237-043d-4938-87ae-bba7ac16a774
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: b87ac05d-3d5d-4803-ab6e-2be5a7259b26
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 02e36c98-a26b-4e09-8ebc-037ca71532cc
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 849ad6c0-ce5f-4add-834a-6f6c72713bc7
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: e2f587a8-8b77-414c-a01b-17da55df315c
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 227e213e-dcc3-4abc-a456-9881c9d1376d
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 55af41bd-f8f0-4b18-aec1-3daa1903ebe2
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: a671783d-f6f9-4e63-9bd4-d99e647545cf
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: b0350bc0-f53e-4780-8646-73815a665fba
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: f396b869-733b-476f-8d06-a2d2f9db75da
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: d3a523aa-5d56-44bb-a0c4-61377fa6aa06
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 6f42f55d-825e-4679-928a-7f5f03af283e
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: dbe76aa6-ec9e-4ad3-9766-1cf868634740
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: ecc5bb3d-14e4-444b-9cb2-fdd07befcf30
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: cd69ec75-046b-409c-ba40-aee4b8e4af21
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 40b09e9b-2230-4dc5-b78e-52475c81f555
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 9958520e-82e7-4858-98b4-ee4c8e3367ec
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 06b6fd17-3be6-456c-9443-9c2fa48243e6
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: e5afd615-de64-4614-86c1-7858cb913a38
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 0276e8c7-bbfa-4bc0-9b5a-57d90c641536
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: b5c7912f-dd27-4ede-ae0a-0d633a8a5693
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 83c760f0-0df5-4f46-8de7-91f70df9fb62
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 7098a3e7-dab0-427e-ab0c-67a1b79d85cc
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 3fd4bbb9-a29c-4aef-ada1-0250acff73e4
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 41acb91c-c4ba-4d5a-b390-62e33c6829fc
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 18a26567-7a53-4d48-96fc-a8af133c842e
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 72e6a442-eac1-460d-b56c-7a2c678e6090
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: edeb6785-4948-4044-88c2-e39375c561fa
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: fc183b8d-d389-404d-971e-4da8b0e9e79d
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 6e7c685d-b220-48d0-8163-154e6d9489e4
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 7f5a480b-68b4-4be9-891e-121e9dc6ef72
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: cac3fc48-7f8d-4b30-ab85-60b93633f4a6
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 0cf60159-f499-4e82-a4d1-53037a731fca
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: cd28dcd3-c618-45f0-9b55-afe779812a42
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 90ce05a0-bbd7-4b86-bd75-8ca3ca4c2295
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 3d4a5578-4023-4ba0-ab42-83b1a07d7d69
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 9786def8-d49b-4c4e-a264-5d9f324ea4cb
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 54591313-aebe-4c5f-a1eb-075cecee34c7
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: e092b9a9-3f4a-4c99-a7b6-7d1647197274
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 0be30652-fc65-4119-9ce5-65a30699d617
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 9abebfd1-8026-4770-9c1f-edd9e22023af
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 8aef914b-b209-4c65-b45f-35a9df49a413
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 4d2dfcf4-056c-4c1d-975a-fcf59a9097d9
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: a6c169aa-4dad-45a3-b17f-127e657b72b6
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 09f047b1-59d2-4fa6-a795-f97930ff4689
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 0143c3b8-9ede-4fea-be71-f2caafb2c99b
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 13627207-ffe2-4c86-a2c3-a922c06a574c
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: ba35a478-c42d-45aa-ae16-67e7918366ab
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: eb6cff62-dbba-4a43-8df1-736746eb2262
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 846c5955-01b4-4b34-ad04-2bafc62bf6d9
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 8399c15b-ecad-44c8-bc3e-38509c925248
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: c84730cb-c3e9-4b36-acbe-cbaf5413025f
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 5f8b7460-147c-4b86-915e-182aa3f3ddd3
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: aa791c9c-3b10-458e-bd1e-2aa4b1f7856b
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 076d1b93-baac-4b1d-bb5b-cdb556efd4fc
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 3a524442-c62b-4e0a-8397-ad97342a0150
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 011dfc42-38a0-4350-a35e-a092eeea1438
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6eaa8ed1-4613-4762-ae87-93697e3606a1
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: a8941cc9-4fa2-491d-992b-e376f09b8a4e
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: d6405611-55d7-49e1-b22c-84f36415ce13
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 18d87c5f-6ecf-48b5-98be-d7da21f99630
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 6e966783-3ef2-4818-8a05-64573340ef7c
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: c697cccf-e0e5-4f62-b0f6-6b03b3b3b04d
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 69c3e9e3-be0a-405f-88a5-2b962a873552
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bb1a5036-d02c-4659-b66e-ccbfdcdafa5b
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: -1LL + (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 93bbc05c-fb02-4411-85b0-a4878373c961
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: ee65385d-9ea8-4f6a-bc05-7d3bf301e171
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 964d24b1-ce07-4cc4-bc9c-92a4f34e766b
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    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: 6327d590-dedf-4e44-be68-79c374a21d54
    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_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin_unwindbound1.i
      input_file_hashes:
        ../plain/divbin_unwindbound1.i: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_unwindbound1.i
    file_hash: e5903ff87e76f5c38f2f015436bd4a2c11a1411b3a93f272aa9f876a0a3f4d37
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
