- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7058d32d-cdfb-45cb-885a-031fc5528414
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: cb2cb265-28da-4713-b005-c46a0e0147eb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 8ad2b677-b60b-4d85-9c84-ad76599d92f7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: f384b3b9-f8ab-43f6-8110-a1cbacd4d568
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: f7b0a200-5b35-43c8-9338-feb50ae9f773
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: a3df136c-8705-48b1-b205-875e9666d3d9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 87a39ca8-a802-4703-9823-5b2e34f462dc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: cd278e94-ed54-49d1-97dc-f71a48cfd859
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: b6238d7f-3f74-450c-b674-6b5d8f15b492
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 942caa98-dbc8-421b-b91e-e3bdc77bf49e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: fab16d17-3c2a-4d5c-988c-f26cc93bce41
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 6bccf6d2-ac0f-4a3b-90e2-08c5cad9efaa
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 9c064505-cc76-4bb3-87ad-c680315c8b1f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: e2ae8636-de99-4a1f-b672-02493695a73f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: c7de8b6e-1c39-4e75-b750-15d920401df8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: a6432ea5-87df-4259-b614-c7bb28ccaf3b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: a57edd62-3973-4abf-af41-b1a7225940a3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 32
    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: 64e5100e-75f9-4be1-82cf-6a6d16fd32a7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: c2d2ac34-f499-4edf-b3a8-6ebbf5954c8b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 3e432647-eefa-494d-b152-056b0118e9c8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 32
    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: 326cae50-ba54-4575-883a-1c251891d4bf
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 08aa1caf-7f58-42f5-bb13-d2c8dd027e6a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 1008966c-2bed-4c95-ba1b-7c800c8b8bcd
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 33
    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: d6a9136c-b187-4abe-b322-c06401c70936
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 33
    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: 2a5630ed-b046-4f38-a466-9c32df037135
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 226ac0a7-5f5f-47b5-a13e-1025734586f9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 33
    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: a50c4fe6-f38d-4592-bcce-1b1e63e8e153
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 33
    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: 783ee77f-e38f-4a57-a2c1-099a362b1281
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f94f512b-7d8f-474c-affb-57fe3179a6b3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 34
    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: 53a024f9-9dad-4932-8d5a-f66b1856b88c
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 34
    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: 2b79bc7d-442b-4742-8003-4c9f67b418a8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 34
    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: 94a14874-2415-4918-8f9a-7be156a1ea32
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 34
    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: 96a3e35b-8ca7-45ce-8107-6068ac1e9ccd
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 34
    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: ee5bc6f2-69d4-4107-95ff-0bf3cd942004
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 34
    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: d52ae55a-01d9-4ad2-9b9f-4facfc1e1068
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 35
    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: ca09653d-516b-4f23-be04-4a5839fae14d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 35
    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: e3f6bbcf-d81b-4822-a883-3b8176913361
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 35
    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: c4b47378-95d6-4700-95f3-3020fd63deaa
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 35
    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: 54713608-8773-40a1-a74d-b1683e8b832d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 36
    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: 951d7a26-d955-4c4d-8165-2c063185a981
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 36
    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: 6ba4c7ca-c892-478e-a85b-cf4db8a55189
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 39
    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: 43e1cb48-4e90-457f-bf54-b7a46bfe73e1
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 46
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6eef385b-1bd1-47ee-8772-971adadc62a9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 47
    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: cf045f1d-411b-4f46-b99d-36749f4fabca
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 48
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d206984e-db0a-4d15-8586-7f9f1b469542
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 48
    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: 4e58d5ec-1e53-4a05-b779-a5fd614b1399
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e8b2e8d-f532-4b06-95cd-dcd094c94306
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3580d616-bae7-437e-add1-cb1acb48c6cc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b9692d1-840f-4a65-bd0e-022c70fbe284
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab1a17df-8bd2-48cf-868e-ccaedbc1facc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2de806fa-dfed-4d9b-8e40-371fb704539d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03e7f50f-2168-4186-b37a-2255314b48eb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 697a60c8-d9be-4fed-8a49-eabf38db3d76
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2f5ce7d-9ba7-4a03-ab2d-7f95aba88174
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99d1d84d-d7ad-442b-9322-46d8ad51e93a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a48b46f3-f521-43f6-ae11-526daa12491e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 44251516-075a-4618-b559-937ba2823950
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: b6283e8b-dc28-441b-b7ee-44650fecab37
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 7c6b3c70-3448-4330-adab-8aed14338705
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 6e0c7b9e-7ade-47f8-a7a9-a9319d7a7b30
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 298f4064-5dab-4e19-bb66-7adefd07cf7a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 0c238f88-6b34-488f-a136-5906c956b947
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 6005e663-467d-45b5-9981-7c648adeda8d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: afcaf98d-02fd-4773-bf26-13d226209585
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    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: 6f2db0e4-06e4-4b86-8e61-c7c156338b89
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/divbin_valuebound5.i'''
    task:
      input_files:
      - ../plain/divbin_valuebound5.i
      input_file_hashes:
        ../plain/divbin_valuebound5.i: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/divbin_valuebound5.i
    file_hash: d02047a3b9d197f6609f19d430d458b8d82d1972f1adb7857eb26188e13a592b
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
