- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d866e163-b0d8-4041-b028-52afc8e14a30
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 1ce34620-ea95-41dd-8035-d558380e6979
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: d74dff12-4493-4d6a-8993-d479b0469ee7
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 09c78b45-b92e-4436-aa7a-db3973983c5c
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: bcdc329f-555f-463f-9779-788755ea67fe
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: aeafb41c-ae3a-4108-8fe6-18ee3bd2a343
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 245afc43-a959-4c95-a3f4-161f21b52307
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: f779b116-579c-481c-b014-b0c6d80d3f02
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 80e01000-8e05-4989-a0fe-f6a66061088f
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 7184253a-a2b3-48d2-b82e-c75194b2cefc
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: a822f5c7-e564-4ba4-a817-05a36001299e
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 3a65ff11-608d-4d75-91d6-8cc5aefa366c
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: ba266f54-4492-4520-bddf-2ed62c25959a
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: e554a5fb-bd44-4984-92ea-7099c4f648c0
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 42c92fcf-993f-4023-a308-e1ab718fdabc
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: b36b4cf5-d984-4c6e-b01b-2c5f84b1b992
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 7eaccbb4-d02f-4bd6-bacb-7d9253d748a4
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 4ef8c197-0e59-4395-a054-a489f741f3b5
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 30e674cc-7d0b-4c58-9658-42f1b73c0b2f
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 337b9001-e3aa-4e94-aabc-3b3d4bd2ac53
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: ba441b78-6be3-419d-89c8-06739c937c6e
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 7edfc285-51b1-40a5-a4f1-891a7c2d8222
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: daf7cf8d-0c59-4831-8ca7-bcb57a78c7bf
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: f3ca9894-3c54-4fd5-b0ed-877281c92892
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: da0a462f-a4b9-4b59-be68-7cdd1c394c78
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 61f8f8fa-14d0-4133-a2eb-8b342ecb1a08
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 4dbf5ca5-1ea0-49ee-b286-0ff64cb81b2f
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: df1a7227-b0f2-4350-8b1d-2f2b45617720
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: c41a3968-0629-4d12-9861-fdce9efea930
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: e8a50fcd-48a4-49e7-9594-96b9a5c490b0
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 630d52f8-edf0-43b0-9560-f58eb34e9870
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: f8bc4dd9-63dc-4593-aadd-d693871faa9c
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 84e762da-100e-455c-8e10-2a0b033d896f
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: f1263470-27cb-485e-b057-aff297a7fb04
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 6cebef4f-578d-4c35-bdf4-b07be2c60431
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 793b5f22-4ac9-4d13-b8b1-20c1b1cffe1d
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: f8a88b4d-2222-411a-b6d9-7ce48ec0a3bb
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: df2fa6a9-dbed-48d0-87ea-eb902a8fb1b6
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 81b7e3ba-9755-4c2f-b02e-3d89558b7623
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 638a685f-2d5d-418e-a188-c832f6ada8c8
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: dcaa0b3d-3494-4f3c-92ec-23e99975fb92
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 683e126a-2950-48dc-93aa-be9c646f4822
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: e5da44cb-0c68-4bd3-9bff-f8b0609c852b
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 23a351a7-40b4-4704-b7ec-17dbed28249a
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 94ddb7f5-deae-4000-9def-041ec6e46e5a
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: e40e84b4-e1f5-438a-af21-0e0a6b8f4f27
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 1b042018-f5d4-4c4c-b7e5-b40f9ef3d1b7
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: dd3be5bd-6034-436b-9e02-cdcb397f5020
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 1e52bfa2-b632-469e-93f7-53632a886b17
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 17e315cf-3aa7-43de-a76e-f18841a34511
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 9c2427db-0a15-4a93-9267-7720e5b2d28e
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 49059306-4318-4ee9-86cd-196fbb83edfd
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: b8658099-2d70-46ed-a09f-93eb492468c0
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: c492b1ab-484d-429b-8f60-2d1b63695d65
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    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: 88c3afda-9273-4dc1-8da2-4a7de57c9cc4
    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_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin2_valuebound5.i
      input_file_hashes:
        ../plain/divbin2_valuebound5.i: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_valuebound5.i
    file_hash: f7372e141bce7d93eac34ddc01970d0d3ee3e3dd05571cb5550acbf38c8c76e9
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
