- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61c414ed-fef7-4c0a-b691-69bf6aa16ddd
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 35
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f60a66b5-db5c-432d-9851-28b883ee75d9
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 35
    column: 12
    function: main
  location_invariant:
    string: b <= 2U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8960837b-176b-48a7-aa90-8a575a316956
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 35
    column: 12
    function: main
  location_invariant:
    string: b <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ffc68ca-61e7-4bb7-b457-bc9b8d932fe8
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 35
    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: 11f6eedf-9ce0-44b1-8c93-2e45f3cab4d7
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 35
    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: f64bee36-2365-4e9b-b619-1d90111dc11f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 35
    column: 12
    function: main
  location_invariant:
    string: b != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9cdc97b-5845-44d3-9229-34a3bcd4bdeb
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 385cbeb9-2ea8-4f77-8ab5-71a0a761a81f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 36
    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: aa099db1-05c6-4174-94d2-5a87424f4f90
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      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: d86926a4-ebf0-44f0-b4bb-64aecb0f78bb
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      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: 144b175d-611b-4536-859d-7d6a36d073f5
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 259c6be1-4ae6-4b47-84b4-ce4a84be0bef
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    column: 4
    function: main
  location_invariant:
    string: b <= 2U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a82adb5d-a926-459c-aca9-6d83ad221496
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    column: 4
    function: main
  location_invariant:
    string: b <= 127U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c4c299f-7329-486b-9abf-32c30fa30cfe
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (-4294967295LL - (long long )A) + 4294967295LL * (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 141ce989-6b84-415e-b65d-820d60eec12a
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    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: 5f86909d-0607-445b-a17f-1f45af2f54a3
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (1LL + (long long )A) - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71072a45-6e7c-4ddd-ab7a-38c4ae9a3356
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 48
    column: 4
    function: main
  location_invariant:
    string: b != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14c37c96-f4b0-49bb-be74-1aed70a3fc6f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 49
    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: 424bef56-5983-44cf-9f5e-985a51cf2ccd
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (-4294967295LL - (long long )A) + 4294967295LL * (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b49feb0d-52ef-4d1d-ac46-840402820da0
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 49
    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: d367b0c2-07da-4e73-b527-e9152992771b
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 4294967297LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4753ca6-e7ab-44d1-b9a3-84cab5efb3a4
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (1LL + (long long )A) - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b3fd265-5210-408a-8222-4b1efff6e39d
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: e580206b-6ca3-4220-869e-1e4d223d0a07
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 19
    column: 8
    function: __VERIFIER_assert
  location_invariant:
    string: 4294967297LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56bc8dd5-be18-40bc-be18-b6926e3b694f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 2ce98b3d-0b70-4a52-84af-711ea672d92c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 23
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: 4294967297LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6526d55a-6eb7-4a0d-9f87-f9c1d61874cc
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: ea22541f-e4b8-446e-af62-e495521f070c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: b5675f15-3483-4609-aec7-2a7493ee046f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 24e9ba29-daa3-462b-a2cb-3b6eefed8bef
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: aaa6dd61-0e7d-4fe0-8c04-9dcb1a389d0e
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 39b70909-f165-4ea6-a032-5953d80386c1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: a8a2e309-0e81-4127-b412-3ce93ce97c7b
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: e90bcb67-7564-42aa-9706-048c61db8cf0
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: f38c551f-d402-4238-bcd2-a166e9678f9a
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 5a2be9e9-a7d3-41cc-b5f2-59ad3977df3e
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: b6d86bd2-b14d-46b1-93bd-eefcaa0f9147
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 08355580-25c1-410b-ae78-5f6d0972bea4
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 71e4f0bd-869c-4b82-9170-65af645beb48
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 26e35af7-3f4e-4385-a03c-8f269af2abd0
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: c8d9a525-67f9-4259-a49f-3eb1c18feed8
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 3e41bec0-3966-48cf-9eac-708c0d923748
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 01f650c4-c9d1-4488-96e4-a6f695f2836c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 34eac221-43d6-4cbd-a537-fdfab448df84
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: a5b0c7ef-5955-485e-828d-a016d2404d55
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: e8d57344-b75d-4f1d-8f12-f0e625f7bb34
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: f1fb1fa9-8179-48fb-8859-5305d9b58100
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: abb1b307-f30b-4778-9cf7-54c457802755
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 447d4c99-1b12-48e0-9341-3103ee189e3a
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: f6509ddc-705f-48ab-beb3-3b759c58dafd
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 0768c8a3-f015-4d84-9896-e4902793d5a2
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 102fec14-3d6d-468f-8356-9cc1d37fcbfe
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: f97591b5-3586-4a69-862e-ea8467e53421
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 8bf62781-7b85-418a-8dd7-b26e8d474dc4
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 493f347b-c022-4a48-ae53-0fc7f679dd72
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 3febb6e9-aaf2-433b-9afe-ffc2857cbcf1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: cbd3da52-1f26-47bd-ad02-0675bcdb455c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: b59e97cd-b065-4313-8e97-c0a52f5245d4
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 88b0f215-699d-452b-862d-db45866abbbc
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 8e9ef928-123a-496a-a4bd-b68cc5cbf6c7
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 4815ca19-b093-462f-a874-5ec7ef679af4
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: f1da4eec-dbcc-4471-ac41-d7c025938528
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: c1208be2-1048-4ce0-8a75-c299d6853dbb
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    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: 3bd2f755-d41d-4937-9adf-4fa0fea5dd50
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 33
    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: e0ca7e11-2c78-44a1-a340-508bba22934a
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09fc8afc-5e1c-4187-9765-492ab4306738
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ab3ed28-c0bc-454f-81ae-93f1f9da6fe1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 63c8bb42-fa74-4c97-81de-d2e2fdb20182
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: b <= 2U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 37c78b85-d1f0-47f6-9ba7-0890a514dfaa
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: b <= 127U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce6b0d5a-3b95-4d7d-bf01-f99565ba41bb
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 62eff81c-ddb8-4089-a9e9-2e25061c7e82
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eb5f6113-ac1e-4a37-a9d3-7a4d55b1b4a8
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    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: 5213a100-8fba-478f-a201-9412d4268422
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: (1LL + (long long )A) - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a029247-d903-4327-8770-3724b5581cb9
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: b != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2954f180-9ba9-45bf-82b0-40a7a6ae6ff6
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2755be1-9785-460a-a07c-e516bc1b22b0
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 49b7875e-4e15-4da8-a842-02bc9d5f8d3e
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: counter <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9935471d-201e-4562-ab5a-b21ccd55c636
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: b <= 2U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2471cdae-0d16-4097-996d-8d87ff461856
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: b <= 127U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ade95ad0-d382-4942-8e81-0cb2154cec5f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: (-4294967295LL - (long long )A) + 4294967295LL * (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eb24db6d-8f86-45e2-b59c-a25c16fbf161
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    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: dee50ce6-5214-477e-af81-b44982017f3e
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: (1LL + (long long )A) - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0610b34f-63a6-4581-8621-90e897b37a46
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound1.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound1.i
      input_file_hashes:
        ../plain/divbin2_unwindbound1.i: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound1.i
    file_hash: 9b373cbe6be5259af58bbd621acc4a598f97350f51d1b5f9aaeeeabd984828c1
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: b != 0U
    type: assertion
    format: C
