- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e75e081d-a50c-455f-8051-b4a60d01459d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 43448104-b969-4ef7-a631-d3e3c6697646
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 9c68513a-582f-4eb6-b6b5-f5fe347b9a4a
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: f66ca62c-f301-4474-953f-efb01ad6dec3
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 41b45e66-6f62-4afd-bfe0-f5c5a56cefd4
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: ccef29f0-a22a-4114-974d-f7a71a69c977
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: e83795ac-186a-4d02-85d0-05b872833030
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 027ea52d-4edf-4769-bcf8-a5da3e2fa9aa
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: f00a3260-4120-4813-a854-b69068f87be0
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: f90e27af-cc6b-4a80-8dc2-495fed305a67
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: a6409bd4-b1ca-4196-9940-7ef703aaf75f
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: ed33e1eb-9436-464f-b1f4-dec55af8f8b7
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 1abc52f3-f0fe-4d90-b44a-3df7966f1bb9
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: b4981337-d6d4-44da-9e03-d54c2d215e89
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 8e177e2e-fe33-41de-be80-0fca6e8c682c
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: cb946b5c-7e89-4491-baad-615e68b640c2
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 2e57758e-e3c5-4bf3-99fe-c13d5be7d57b
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: ee972997-4c4b-4eeb-bb64-3cf96662ec8a
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: f9350558-0a32-4c6a-9ae9-a45a896c9a41
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 11c4b928-da33-493e-8d2a-8b776ccdc20d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a98a040-e4e9-46b4-bec0-7d3a6e4021d6
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 1b6d969f-4636-4ff6-8ebe-0789b10b4ac8
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25f6ea1e-ecab-42e5-8dd7-a4ba59ba2a13
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e537ceeb-8828-4521-9297-88d9fbab1520
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 2U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9023ce1e-0cda-452d-9b0e-07c116c6aa12
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 42
    column: 8
    function: main
  location_invariant:
    string: b != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a59c547-c2ed-4de9-875a-430f9917f298
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 97a29990-162a-4ccc-b191-4b1329348c30
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 492d4d9e-505c-4d9e-9845-f8271aef5b2d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 3f6074bd-4236-4314-bd51-e8d73e07b0e4
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 0b494c2b-4200-4052-af72-cd7120f5773d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 1U <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34e4a3bc-fd01-4056-a336-65987ad48b24
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3aa8685-3daf-4bf2-8c82-6b21c983376f
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 05065f17-e9cf-4d81-8ad5-315043576af1
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: cb263568-19f9-4181-bb28-01539fb24f2d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 45
    column: 12
    function: main
  location_invariant:
    string: r != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f655520-e99c-47e5-a5d9-bee34c94de5e
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b08431f-5526-4b4b-bb50-071b89932333
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f96b875-a691-40a6-a758-4563cf7c7a13
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bc78d81-c1b0-4559-accf-fa04ac9fb9f9
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d9c3c8d-56bb-4fa9-a62e-c8b5ef209f70
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9051f37f-696b-4072-9f6a-e14667080d84
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6076828a-a755-4d65-b75b-6a47fab3508a
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 134395f7-0545-4c66-ae8b-8bddcadbb5ad
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12de6137-d467-4669-9c29-fdca21c99f3e
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9619fc2c-b05d-4f05-bf97-e2ae1252789d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e2003f5-b535-4929-9a7f-bcf8cd7a0e1d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: e8d533b3-3a90-4776-9643-2a68b77520c6
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 6a8c6a7a-cba8-4ce0-a8f7-5c80e4fd762d
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: d2204090-e926-4dac-b35e-8add5a083dde
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: b87415ad-9f12-4886-a3a3-626cd59c6a1b
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 05dba818-70b7-47e6-a6de-25b186033383
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: ffee11e5-896e-4172-b920-1772e6c40252
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 7e93d984-7d89-4f31-ae96-fab73ddea841
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 35098f5b-92af-46eb-9b56-34bac2382792
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    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: 910bf1fe-f4a7-42f7-ba12-247f80537c99
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 29
    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: c2f774eb-2473-45c7-8736-f538b6b4ea72
    creation_time: 2023-01-27T16:29:25Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound1.i
      input_file_hashes:
        ../plain/divbin2_valuebound1.i: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound1.i
    file_hash: 09575df3d22e9082519fef8b3f639469f79418a93deb54dd64ac9991de61e42a
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
