- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14e551f2-3de7-49cd-b727-098e91eef7d2
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 35
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53512664-a628-4724-8920-a1f798f88746
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 980f157e-694c-4bbd-ae4f-21c9edde2f0a
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 517640c3-f3d7-4cbd-89d7-8060cef715a0
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 8661fe68-bf07-4f9f-87e0-b8bf608148e2
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 36
    column: 8
    function: main
  location_invariant:
    string: (long long )A - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83d48ab3-f76d-42ae-8e7b-fabbd62f3b91
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6ea668d-8eb0-45f5-aded-47f671266248
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 39
    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: 0257ff93-8df9-4c41-84c7-cc3d9ddb2941
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e9d068c-eebb-4aec-90fe-2866f4d0e2ba
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 40
    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: 6b186799-4c88-4c7c-9744-9929acd34cdb
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e72c93f1-0e32-4cbd-bbba-02a38064aedc
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ac78879-1272-4f89-891f-77350de9b4a9
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86e2bc1d-918f-4cad-8fae-51f1864077b8
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 42
    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: f957a275-c04b-413d-9bdd-1a05b5ab77a7
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 42
    column: 8
    function: main
  location_invariant:
    string: b != 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73b7b82b-91de-4345-84c6-3c67cd206a94
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 43
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 701c42ea-d76e-4935-a42d-413aa51a788e
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cdafa9a1-2401-459a-bb8a-2c6f9132cb11
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 43
    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: 62c742e9-5539-425c-bc00-ba75919da055
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      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: b400cb0b-70b6-4360-9158-5ccf4b2d1fc8
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      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: cc55c68a-465e-4c59-b1bf-74aed1eb0270
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )b) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddbf5a0a-0441-41a2-8bd5-77657210bda8
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58c1d957-2b74-4c8a-8492-71ddada5f381
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 44
    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: cc55934b-c21b-4a2e-ae44-78bf9715123b
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 45
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58f4b77d-58d2-4093-b104-8b4f87faec49
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 45
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )b) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81ad1819-c116-463b-9e4d-d16a0d0832f3
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 907f71fe-e6a4-4cd1-b00c-9bbd8c951166
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a8c31cb-97c9-4d31-8531-82d97a92ce00
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 8d58e90b-e6da-4ade-b7b5-a0f323a4b2bf
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 6b4939c4-abcc-418d-86c2-d598d51579ed
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: c03bc962-646e-48e5-92b0-2e5b50b8654f
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: bc9f231d-f476-425a-8780-8be61ebd767d
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 11b37baa-83b2-49a5-b8bc-1c3a7fab6035
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 5b270cc3-b7a5-4a53-922a-3bf1de27d0fc
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: a156aedb-1a05-4144-b92a-538f4db6025f
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 04b458e8-a10b-4e4f-93b0-57dc49d0841f
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 0b9ba4d2-fcdf-4696-b7b1-3f57be368943
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 01cf24a4-86c8-45e6-8300-12fb0c210485
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: e30929de-4a45-4bdd-bfb4-347037af0d80
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: f68dbe69-0de7-4e88-a26d-464e4edf9f9e
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 4546c275-027b-4c69-87dd-dad2ff68003b
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: da9a6b72-18c7-46d4-9052-3aaa00104b99
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 24bf961f-8f1b-4a2b-8e7d-6b88d0fcc83b
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 98f654b7-52d7-475d-9d43-e52480bd7542
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 5dacfbb9-c1ce-4738-9d75-80ce935c3734
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: c9d674d1-a8c3-4cc1-8837-3a0dbbfc52ad
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: a252213c-e8cd-49bb-afb2-d24127ab641f
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 10d6e6ab-974b-45ff-9ec9-062a11713f44
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 6168a8da-455f-4c06-8d90-2d268a8c8f55
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: c5455773-419a-4279-a707-0cdb7a943000
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 58d0b4cb-b9e2-4a52-8a2f-1597c35f5032
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 877afa44-d9ef-4a3b-b486-9e8237a320f6
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 1748ed03-6be8-4f18-ba3b-085bb3e285c0
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 9bde722a-6502-48d7-9314-b7979a03eb4c
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: c23a3e05-bb7f-442d-aa89-442710eb95cc
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: e701e86f-0726-47a9-a0b6-1a479b680caf
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 06d7f81f-7978-4d90-a3f1-1c68ea11e170
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: f68446af-62c8-41f0-8a8b-c284ad49ef56
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 3ecc25c0-df38-45f3-8d34-ef3b4c7994f7
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: ec28d777-24d2-462a-b5f5-2ff89e4332f0
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: ad92f634-7cd8-476f-9bc2-8bf303d95e10
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: dd9c37ad-bbca-4fc6-8136-3b407a7a94cd
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: a829c74f-b0e8-4840-82ff-162529c096e0
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: e1b8ce0a-f02e-44b4-9b9d-d04a3fa5166e
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 7535f27c-3128-439e-88f4-ef7bcff23499
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 54320a0b-e456-40af-b1ad-1655051b8c6b
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 2ff2d721-9a1c-4ced-a732-f3c35df402b3
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 5ee767f6-15b0-412e-b2ad-e72e214d38eb
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 8852d467-8c8f-4144-b33c-abc6ac601380
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9ac76bb-9807-48ff-8224-1ef1e949e636
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 07974fe9-59c4-43ac-9826-588793339cbf
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: eb2b0f8b-aee2-4e6d-8ba6-e290b1ef9f15
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    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: 5b08fed9-ada2-4ce7-add0-573dad6d482b
    creation_time: 2023-01-27T16:29:24Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound2.i
      input_file_hashes:
        ../plain/divbin2_unwindbound2.i: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound2.i
    file_hash: f2c97cfaf178ecbb63eaaf825cd5ea4b5be1bf37ecd5b20cf7e400328e1cd168
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
