- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9583003f-432e-43a2-9cdf-c67c69286e10
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 05611efd-258d-4ab3-9e97-0b3e692a5ba8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: df2d1d6a-5252-4bb5-964a-fe4907d25edc
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 4d8802dc-74ec-43ea-9ae6-9942fce9aff4
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 7de04ff5-5034-4a61-9e51-25e03c054364
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 7d6012bf-6409-427e-99b3-fd09972091c5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 84a661db-ba78-44fc-a5db-f5b0c902e2ef
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 52a19314-a614-460c-9a18-cce0f1cca912
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: d04d7d3d-ff47-435e-ad2c-d8115be43253
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: f912f231-c700-4639-8f69-f7eefca32c14
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: e120e5d7-a1f5-43ee-8dc7-44013929f0e8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: e0e7b4ab-a340-456b-be44-d0f31c2688a7
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: a526cb7c-ccee-4697-8252-842345200772
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: a61dd9d1-f3e5-47d2-bdf0-12541f9e3bce
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 059bf49d-c269-4924-bde6-e1b528c2c14f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 9833fad9-6326-449f-9418-2633a6fc3561
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 98744c8f-85ee-4f49-ad55-f3085f658cfe
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 8a8fdea9-a22d-4e99-ab7f-36290ed3d50c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: d448a7ac-ccdf-4d7d-a1e4-ba834451c857
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: c9bfa5d2-1c21-4b19-9520-bed94bf79272
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 30e1352f-62f5-41db-992b-611de385dd3c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: b0705376-d5ef-43c1-912b-6bac514f188f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 21490d41-188d-4f03-beca-be2e72199506
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 3a25a109-5ccd-4e3f-80f5-b1c8c4564580
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 922abb96-3c8d-4f78-babd-f2d70359ac12
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: e0f20662-820f-450c-9903-03d24880b09b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 31a6420b-455c-42c4-867a-1b0dd25d4644
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 6ab14840-f641-4ad5-912a-e3d38ad03750
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: b11e58d7-eb3a-40cd-9a97-c327d891f07e
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 6c4f20ec-f180-4476-9040-88cc3903991c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 0940a171-47dc-41a9-855c-4b4509ea6076
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: dbf3ca17-55fc-4039-beae-7017e6889f85
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 650cb998-7b32-4ad4-9370-c77ecc6a1c61
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 6e8debc0-c9d5-4b5c-89c0-00f89cfc5d91
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 6075c6cf-7a25-4616-90e1-ec975c1a7458
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 71a9b6ed-8bad-4651-9faf-733e44e1784c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 900f7079-c2b0-4271-9a4a-df6ea5cb00a5
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 921ce4e5-3827-41de-a7cf-173c80ce6b2a
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 0b37c5aa-02fb-4a75-bca6-15a5fb97a71c
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: d67f2f4d-7926-4880-9661-99869892ec1b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: cce0695e-6747-474d-96bb-add81af01979
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 93982ee2-f092-4298-bbe8-f8a8b85db8ba
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 3c406397-646c-479f-9170-21853068052b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 75b1081f-9816-46c2-94a9-ee459c8256e1
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: e0b752e8-009b-4902-b3c3-fb634312048d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 189256a2-fa54-4a6b-995a-1318beb3e8f0
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 55c5aec2-6c17-43bc-a616-bb86ff8e4e67
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 9c88f303-5bdf-4c5e-8d3b-720c8ec4c55d
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 47d76621-798a-4d64-ae34-84d0f0ef025b
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 0a620d34-b403-478a-a23e-2c6ba586f5b8
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 1a61d529-3179-4c73-b062-34995b8e5a5f
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: ce6d4b75-f99d-49e8-81b5-023975032a37
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 86894e50-b641-4a47-bf55-1066cf1840ba
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 80a7eb30-ed5f-449a-becb-00f36bda12b9
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    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: 400fb653-6f7d-47e9-b222-79acd00612d2
    creation_time: 2023-01-27T16:29:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_valuebound50.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound50.i
      input_file_hashes:
        ../plain/divbin2_valuebound50.i: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound50.i
    file_hash: 698c604312f3eb09bef7f8f6e092d43de99877a411ec8f3c76598811466d02b7
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
