- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb293632-3fd7-49cd-a6a4-fb9b9f7aa1d6
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 34
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe815d40-d10f-4478-8c08-0c0aa23a8d76
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9008518c-7016-43ad-be19-49d9d8772124
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 35
    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: 9b6df38d-777e-49f3-9b4e-47edaca17587
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 538782b9-df11-487c-96ba-0615fd6f61c9
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee65827b-3a1a-40b5-b222-26784b321839
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d98dfa3-8e67-4f1b-a2b1-d75f469a7709
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef970560-f25a-456b-a288-836e29421849
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 476da3b0-f27e-41c9-a286-5f93328155ca
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96e53cae-30b3-4eaf-b7ac-e8ce8907e90a
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19aea490-fda9-4ee2-99be-d43630cac9c5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: b != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07f34d2c-a559-4759-97df-153ec2a02022
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 41
    column: 8
    function: main
  location_invariant:
    string: b != 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcba63ef-69ef-4721-8b97-73245312f5bc
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10129684-081c-4512-930c-a42f61fb8e4d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5b6c9d8-e421-46ae-bc41-c6c3330109ba
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad51c53b-c54e-4125-84eb-b9baa9584053
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 43
    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: d970d37c-e8be-493c-9020-d0450a074669
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d5e10c3-81b5-4f36-ba56-31b525b0bccb
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 1U <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16bae666-adbe-4969-9af2-7294c0b5369c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 362abbb0-0415-475c-878f-7ba53e256f2b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 44
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2033266e-e77c-418c-be91-0a72cbcdac3e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 0e685e4c-4f6f-4129-9b84-234f1b84876f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57466d00-162d-46ce-80c7-d471e270692c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 44
    column: 12
    function: main
  location_invariant:
    string: r != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44243451-c8ff-43e7-ab18-2967a9439fe2
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 47
    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: bedd7bac-c202-4081-adb9-628a536e240e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da52b211-0fdd-4060-8346-db26c37cb2f8
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 1b7d035b-f874-4895-96d2-362c3b63cf1e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 72af2576-501d-4c80-b26f-3f768e2a9184
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: dacd9923-c822-4b2b-906c-5e88ed8419ae
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 74e6ceae-d1f2-46b5-aeba-727dd9de9045
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: d20c8371-e290-460b-a752-7e30f887f57e
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 4741c540-3a2f-43a4-8ea0-e7da11a9cb01
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: c1603d77-cc72-4d7f-a37c-98e6edbac5aa
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 29655a7d-c552-4844-ac18-f2e251b0dbba
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: d3a88832-9699-4d15-a6e1-4ba015a219d0
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: d28bd230-a9d1-4345-948b-554b0ee1a2e7
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 5a98deeb-1b60-48d2-9a28-6c3515fbecf0
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 12fcafa6-393a-43de-890c-66d9db4aa330
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 46b1f421-b15a-4c10-9f3c-b2e20ac37872
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 9b788667-2d7d-43a0-b831-b1cb0577f3ff
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 58a1e190-7a7b-4ad4-9c50-0c7aba2a215b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: dadccf4c-6e63-4748-9bfb-4f7683dd408d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: e42843b3-d20d-488e-87bc-47a23a151217
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: bd51a473-c822-4b14-b6b6-d2cdfa20b686
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: e095f0af-7647-4773-b9c9-4cfe8d62bbc5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 521b98bf-0e20-486d-890e-c95a4753d2d5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b58bd981-4ab3-4bdf-8e05-d12c5fed32a2
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 79f3acd1-f82f-4c2b-9197-cf7d104b7274
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 54893d93-627d-428d-81df-73669892546b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 6bc8bee4-02ff-4c92-9a04-d5f9c095426d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54ffbd56-c36d-4e6b-9fa8-f840cfc3e48d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 0e67b7df-9513-4899-945f-2cdec8f384a2
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 9db2930c-fa3c-43c6-a745-035c89ae80ec
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 2dcbeb28-c6ba-445e-a3b5-77e5d1e48127
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fc6e8c2-5160-41a2-8918-5050da94151f
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 39019c27-3f06-4453-86cc-4b749237ab86
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 8688c8f7-0dde-45bf-b8d1-36b7ef4b16a5
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94194392-b16a-46b7-b69b-e4c6be19156b
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: fb95ce7c-abc3-482f-9591-0c39564ec5fd
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: cf75b8c7-2d69-4db5-96a5-2ec04d0a423d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: feefd311-c9e7-4461-8c56-359dd9e5a947
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    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: 5f1e887a-c409-4c8b-b3e7-fe959b0f6a20
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6ed2251-1edc-4c8a-8a6d-0a8d9a2a3d92
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 32
    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: a1571ba1-1380-4367-9df7-6d0525935bab
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d36881d-5c89-46cb-ac60-3b1463f1bd7d
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 1U <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f9c3dba9-c718-436d-a646-b91480c3cb6c
    creation_time: 2023-01-27T16:29:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2.i'''
    task:
      input_files:
      - ../plain/divbin2.i
      input_file_hashes:
        ../plain/divbin2.i: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2.i
    file_hash: c7e3f11d23b462949b18ec2057853f57240b0651aa6fb66cf591585739df9d3e
    line: 37
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
