- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8e413a9-26ca-43a4-8500-66daa04d307c
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 2021fb35-5474-46a5-acbc-08a4848027f2
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 544b8a9f-35ad-4916-8314-67fb98a9a25b
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 38d46ae0-6c47-4257-b4f0-485ed298ca4c
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 8c3ef44d-d041-4021-a2a5-bf105f6d8ec5
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 93569401-b636-4eb1-afe3-98124f98c260
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: e24fc431-bc8f-44ad-9880-272b0a14c850
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: b7e3893c-0f71-4033-86af-b0cff9ca2e44
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: b029d334-74d4-4d0b-a4ac-aaca29df3c91
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: e4e41a69-aadf-4cbe-bbcf-8bc279b0c0de
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: bd7a8f3f-e80b-4416-80a8-4aa7c609d810
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 37aa4e4b-7d5e-46a7-a3b6-9c7784e64bcb
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: f9818910-a438-48e4-9078-986405a84dfc
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 0e9c584a-1937-4b53-9323-d82e485a8055
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 57184599-961a-4581-9264-1d4e7e439976
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: c6cf9e39-b55c-4099-bf4f-9fc82ef94a3f
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 5a355bcb-30c6-4de5-a3cb-a42cf7e27227
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: ba60e65a-66de-43ec-8efd-85cdc0b052d5
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: faae762d-91fa-4240-be53-e9c37263a149
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: ee250748-102d-4a63-afc5-e1134db768d9
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 743a2abe-c224-463c-b066-a647decd135d
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 4bf17feb-b7aa-4e4f-905d-a75216a9a03f
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 7ae939aa-b2b9-4481-a1e7-6249508b72c2
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 6aa921c6-041f-4a46-84df-7667032e2bbd
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 5a710d49-c8ad-4887-a6b4-d26a9b4347c8
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: f461c771-bc21-4ed0-bc74-4ac14325a9c3
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 33a9a3a5-ef86-4844-a512-c40c959f881d
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 68926520-2246-4ddf-b283-4f77548ac73d
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 5aa001bd-4f18-4a95-a3b0-3f53a8139e25
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 6e71468e-3a1c-4525-b958-082052da194d
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 15e3ebb7-813a-45bd-888d-8f8e018acd74
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: a7029da1-24ec-4595-ae22-c81a5318c6a0
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: fdb4271f-614e-4fec-894c-2e90286dc4d4
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: f106f308-451f-4fb1-9e09-a92bd4dad716
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 2ae76235-a520-4d01-9e2f-8ff5b36d8c65
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: f5964db3-39f4-4b22-8bef-ee8ef34b7a1a
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: fcae7783-9f0d-4c85-81f6-8486d1b43bc5
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: f81dec60-f223-4bf7-bb36-b0b1b767ab70
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 3333953b-d76d-46e5-b1e4-9d66a1b85166
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 0775bca1-560b-438c-82f5-5ef4b1bcbef9
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 4e88a0c6-217f-436e-a6fd-283c8169f800
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 8f48e4aa-1888-4a6c-94c7-83a8f0785168
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 301deaa7-d363-4a05-9ac2-d59b499d5e72
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 347a59f8-7e3a-4d48-a43f-52785f1d7e8c
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: a877c43a-78b4-45f9-a5e0-161ab9783db8
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 764d112a-1add-42af-9185-9a79a9cc8217
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: ad906804-c294-4fed-8f10-6efcf0749e9b
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: e6af9524-e8f1-4e2f-bc0f-0df69838deb5
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 4f86809d-0f0e-4f91-b60a-14be793d49ba
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 8ea5796c-51c7-49f5-be63-d8bfe00abec5
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 8301df60-cecf-46c7-a86d-13e492d3ccb2
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 9440b33d-6f90-40a7-9917-06e5060464aa
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 18609964-a9f0-476a-9489-189301e75b59
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: d7b8a0a0-83f9-442c-b9aa-c7c658aa4a0b
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    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: 0330044d-05bb-48f7-934e-60086a312d06
    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_valuebound20.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound20.i
      input_file_hashes:
        ../plain/divbin2_valuebound20.i: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound20.i
    file_hash: c533ab673c7ac44f09cf312108422da4b4eb94a047fb46aaa19b12fad5dce8e7
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
