- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32f9627f-0a81-4582-920e-8a39699b5659
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 35
    column: 12
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8e03a5b-81db-48ad-a797-df07b7d22bed
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 35
    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: 652a46af-dddf-4558-8c31-00c1ce78d32f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f42e9269-dcbb-4761-9aa8-442949b2af5f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 36
    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: 766c3917-5c2b-489f-a174-f20f4d49d686
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 0051d25b-c409-4681-b2d7-74c7f94aef7c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3679529c-0120-4c9f-9d3a-0a2d16724f07
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 39
    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: 3240833f-8f63-4dd6-bba2-ed67e8268fa7
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60c165ed-4eb2-441d-ac8d-8b3c22188eb1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 40
    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: c51a3887-4844-46b5-8f2f-8b281339ce2a
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c10ae83-0cb1-4aff-a95e-aeb2af9b9b60
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 0380966d-5b53-43e6-98d2-93ba40101f53
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b75dd88d-fa2d-415a-8399-ffa8f1dc5303
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 42
    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: bf31d0df-1d63-4f9d-a9c0-63ae71663e18
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 75d629da-9d21-4559-9ef7-f642d63de381
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: f91dbee0-7663-4f16-a8bd-36b97cd4ed99
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc7b00f4-d4b7-411b-ade4-25d858f9992c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: c5d99595-81b6-41fe-a095-5d12e9051948
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 459389e8-ec3b-4f58-8d9d-1bba81263e99
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1c46dae-8082-41ea-9baa-eecde27b3223
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 1433d0f9-1e6e-4e8c-b4cd-ac8d0a300b01
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7492b997-2a6f-4bcb-a9d5-11b66cd252dd
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: fe190348-d753-40de-baa7-4bbb2436ebab
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 488a114a-d4c3-4df0-851a-b6b3873a6fec
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: d2796a0d-b1ec-4171-b8ad-9f110f82ec99
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b76f9e99-628f-4f04-b078-792a812cc364
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 45
    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: 2341a913-aa33-4ffb-86db-a4364a816fa4
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: d57c6c58-6771-47a4-b80e-95952e0b3899
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 49
    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: 2db7ad93-9bb9-4536-906d-b1fd9051ce6c
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 2f3f8937-774d-47a8-9a71-dfa39cdcdc20
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 4bb17b78-faec-43f4-8d5b-db3e901b4432
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: f7cc8ead-8e0c-452f-b430-3c8a82a92b82
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 39f740b5-6b18-40f2-a87f-45ab48777d27
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 6bbe9f25-54c0-411b-a10f-bd4f33cb89da
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 94231d79-8b71-4585-8bb6-6ff4f4eb707d
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 91e63a44-f075-43a4-af24-edb480619c36
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 90904dd1-130b-4294-a472-662edd0714f5
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 6d731603-77c2-4aa5-ab6a-b16a7abdff26
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 00ff0484-5eb2-486d-987a-ad84ae50e5e1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: bbde46fc-5959-4f63-82c1-7112a00e24a0
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: b81994c0-9a6a-431e-90fd-5034534ccc15
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: b22edbf2-e027-4d36-814c-51c7b4080fb3
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 7e032a4f-1f5a-4506-8644-471df50f5f5f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 35ece312-df2e-44e9-93f6-0746b328e8a1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 76e5e53d-53c5-488f-ba6d-6fb0ad781289
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 6705a01e-6ab8-437c-8a10-c944b65d881d
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: c186d615-0a0a-4373-93bf-57dd7db2d289
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 64a6e88a-42e6-4178-b153-8e6f2959cda9
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 7626e594-7aec-4aff-a189-0b73be04fe1b
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 7a5ea5bd-4a96-4f73-8c59-dc88a5582f95
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 94809d59-3f3f-469f-ab14-37980d7edc4d
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: d1a2ef38-a00a-4834-b467-09a263151acc
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 454c49b5-67fe-464b-8456-5b457460e230
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 388d11b9-c542-4b8f-b886-2d83489ebc88
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 0b968f7e-0514-4e74-ad71-f4453d345660
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 6b013ca3-b16a-444f-aab8-051c0755982e
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 949a4ba3-ea55-48d2-814f-08f2ca94222b
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: b1d4eae5-acf9-47b2-bb5f-6202e5bb68ed
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 8072e1d7-8e2f-4615-a8bb-8cc27fb40f1e
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 445766d1-07fe-43a8-9c4f-4e0745326d64
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 33e79eb5-e025-46f3-aa5e-f001174d68d2
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: ece0f8ad-407b-462d-afc6-a1cfc583f954
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 73d1a3c0-3a56-45d1-9c51-5f87b31dfd96
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 33
    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: 7977355f-3ce9-432e-9c03-550dd4c2fe15
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    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: 9c7a0e24-3824-456a-8e15-5da2032b7808
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 33
    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: 27b49bb5-5c7a-4433-a179-f2fd8c8247a5
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 33
    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: e86530d4-9809-450f-8099-2bf66545a045
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 026d2ba3-cb4e-497f-9790-832b913607f1
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 11
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a0295461-7e9d-4c6f-809a-b8e0361beaa0
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91096f55-0665-4060-8cf7-7506830916f2
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 34
    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: 556da364-820c-45ca-8187-726a5a8f1068
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 1 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3ef4ce5-94c1-499b-afbb-6a50903f715f
    creation_time: 2023-01-27T16:29:23Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin2_unwindbound10.i'''
    task:
      input_files:
      - ../plain/divbin2_unwindbound10.i
      input_file_hashes:
        ../plain/divbin2_unwindbound10.i: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin2_unwindbound10.i
    file_hash: d7b32f819b918e072cd2f6b8ef11cf08c33c51198307cb8de75af009db97bd7b
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
