- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fad0484-1143-48ed-aadd-07f8672b5f3d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 36
    column: 28
    function: main
  location_invariant:
    string: -1000000LL + (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f333efa2-304e-4330-a29f-8cd42997c610
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 36
    column: 28
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce5928f1-ec0f-499a-bee6-ad2c8768de98
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 37
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4de18990-bc1a-413e-8fc6-62fbc618ea7c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 37
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31e50420-79cf-4682-be90-b9f4aad37be3
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 37
    column: 26
    function: main
  location_invariant:
    string: -1000000LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c07bdb6-c471-49e2-9ef6-44d567f250a3
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 37
    column: 26
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a37d3c2-874e-40a7-8c58-2a514be6c87a
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 37
    column: 26
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 001bd724-d811-4422-a15b-bb5952322e9c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 38
    column: 5
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f2a8f79-bf15-4f54-9d1f-e63ccf7553ea
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 38
    column: 5
    function: main
  location_invariant:
    string: bufsize <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1ae003e-31d3-4d0a-b24e-bafe031aa575
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 38
    column: 5
    function: main
  location_invariant:
    string: ielen <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2abe91d-0cc3-42ac-b94e-14b099d2df65
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 38
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a790c3ac-1800-46ae-b3a2-79ce5e7016a5
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 38
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fd7d82d-6821-41e3-8226-db6e82c1235c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 38
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0d486ed-07e7-4ea9-b2be-bf51e22321eb
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 887ddab7-e6a9-49b2-8e85-783be6fe254c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78cfdb0c-28d0-4fdb-acc1-8cf8f88d61e7
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: bufsize <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf7c6694-705b-420a-9103-087ab6060b3d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: ielen <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 439dba79-1812-494d-8271-2a08ee5f95d9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30c0f88d-afea-435f-82c3-dc41790d9f1e
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36868606-949c-4a47-8c27-cdca8d35b0cc
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 069a52b0-aead-4aca-9c34-64938992f25b
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13f8067c-db9e-43bc-9876-e4995b5fbb5e
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 39
    column: 5
    function: main
  location_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c789c76-9566-484b-9513-d5d76178865b
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63149580-05dc-475b-bb3f-edc4f3eb444a
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: 1 <= bufsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3aae552a-c8df-483d-966e-aaa4a5008064
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d9cecd9-6c30-41bb-9919-15780dcceed9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: bufsize <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 289cd609-c222-457d-8770-3ab62df20c71
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: ielen <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98d80e98-6862-4e7e-84de-a61e2debaa98
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13fc2f71-90ae-42c2-aa06-915801355e3b
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa1b21ff-c37f-48de-9ac8-b8a3b8fa4a12
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81d0dd3d-42f2-4b6b-a5ef-ac1afcdf5472
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84feb1fa-4a9a-499d-9da1-9450a3a76769
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bd2598d-7775-45b9-be38-0719cc99618c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14e907fa-6d75-45d9-947b-3759401fb288
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 40
    column: 5
    function: main
  location_invariant:
    string: bufsize != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1badb09e-010c-40b7-becf-9ba0fa7c984b
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80e99cd0-e300-4735-9f32-2a8f6eb92a1d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: 1 <= bufsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7caeea5a-3d0e-42f4-955b-07d4fc7810d6
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: 1 <= ielen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c0ed29f-c0d4-4878-80bb-d451cf866314
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5418392-3abc-4b09-ba56-1cd365f2ce64
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: bufsize <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80889784-79b6-4ad1-8074-06217d6c9a7b
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: ielen <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fa43416-7130-4c71-8aca-c45c8896f90c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 291c6aa0-2b8f-4b49-8cd3-ad4d2e0ad0e0
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b71b0c62-f984-40ed-bfde-a237ffae3d66
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1da88c13-8647-4345-b6f9-db89876ec35b
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73fd1ae5-aff8-4f65-9fb6-f360963b77ee
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8116606-8aa3-4e2c-8949-52816f83adc8
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31650322-8835-4250-8ba3-5afe387e80a5
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78bb6574-5978-4c9e-8087-9619d0265804
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: bufsize != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3aef863a-dce0-48da-81b4-592dae29a813
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 41
    column: 6
    function: main
  location_invariant:
    string: ielen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2da870b4-e248-4f27-9ddc-63155fce4fec
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 43
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62e485f4-76d1-47b6-9f24-ffa03360f711
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 43
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9923ad8-8296-407a-b954-6886d1e87e7c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 43
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9e462e6-9092-4671-ae5b-e3afd164c619
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 43
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fc1fcda-b4ea-4f66-ac38-1bc886454836
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 43
    column: 2
    function: main
  location_invariant:
    string: (long long )bufsize - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74acc93c-75ce-4298-9fd5-bc5a3cc8f409
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: 1 <= bufsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d11dd17-5869-401e-af99-3c92729f824d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: bufsize <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11fe8973-6e29-461c-81c0-2347948243fc
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b77a5ec-1a70-412d-ab26-f1708de61a77
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd37643b-3edb-4484-b718-29842b0a04d6
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb08ba5d-9ddd-41b4-9169-44a2e644809a
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7dde8427-8f12-4d65-a051-32a3348bb828
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: (long long )bufsize - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55ee9dfc-87ae-45d0-b07c-68c8cc9c8084
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 44
    column: 2
    function: main
  location_invariant:
    string: bufsize != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30e00ed9-8020-48d9-afc2-91a8910cb110
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10e1bb28-0838-4452-8076-53e5f75537a7
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: 1 <= bufsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d38d6da-ec4e-48ab-8076-f65a9f6ed961
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: 1 <= bufsize_0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e826b38-7e88-44f4-a172-9a07a60c83f0
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8babe49c-36ee-4b30-9c28-4fedc3d13d82
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: bufsize <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d22676bd-5cc7-4818-8648-d21711eb22c9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: bufsize_0 <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5fbe614-fb7e-4211-a4a7-114d5078ad08
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9248e541-1f97-4fc7-ab20-61d8a15de5cd
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22b0d39a-d5b3-4996-9956-93505d3be839
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4140a3af-117e-44ad-84cf-baa1a725aace
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfdefa89-3393-4064-acb3-56f9f4eb8048
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: (long long )bufsize - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d626e97-a796-468b-981f-59bbd9debc21
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3faab1e7-031f-4966-b271-d2f99e677ef7
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: bufsize != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e340bc70-3534-4aec-b095-8d0ac0cf9e03
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 45
    column: 2
    function: main
  location_invariant:
    string: bufsize_0 != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5250634c-2e5c-427e-bb48-4eabfc9fef4d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: 0 <= bufsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86e55ac2-7691-46ed-b039-cd94938cdb29
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ff56e78-3bc2-44a4-b77b-6573c44131be
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2744fa6a-5ded-429a-aa4e-a8dc6fd162e2
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: bufsize <= 999998
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e6a5195-c948-40b9-8424-80401330f06c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2a76579-1670-470a-838c-c743f3c8eaf9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: (-1LL - (long long )bufsize) + (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2431ff7-61e1-40fb-97fd-163cf07352cb
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c92c9317-19ee-4b34-922a-e8e32eb932dc
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 208cf313-9d05-41ff-ad5a-1b59554424e6
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68689312-4819-4ae9-95ce-bf80ed0f5867
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 46
    column: 2
    function: main
  location_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 572381a3-9f85-4689-b05f-d6bee44fdf16
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: 0 <= bufsize
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44bdc2f7-d5c1-45dc-825e-bebe88672e41
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85dfa0c3-bab0-44ec-919b-ae9391a3181a
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcc0073b-6855-49d6-a394-53b1ee291eed
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: 1 <= ielen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69209a9b-e9e0-41a2-9beb-add3caecd437
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: p <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4450fffd-31dc-46cd-be6c-9944e2ef625a
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 030fc9d1-39f1-48ae-aa2b-4de5529fbbde
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: bufsize <= 999998
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c45acb2b-1fa4-41e7-9cd3-d8fd4e321d54
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: ielen <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 016ef487-f88e-4600-a7e5-98d7ca67cb6d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57a6ecc7-5d0d-4624-b6c3-7029ea97f0d4
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )bufsize) + (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99552e78-68b3-407e-b7b8-a037d9bd2632
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b5b8af4-ef84-4a8e-9791-b27c51e906f9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be1732f8-e48a-40ae-ab98-af6db4b40f94
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bbe368d-157c-4d0f-a3bb-5272657c1969
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: p != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db140840-d649-464e-b98d-e2a9d3c2e4b7
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d8edde2-8fcd-4976-9149-bbf08d5df921
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 47
    column: 6
    function: main
  location_invariant:
    string: ielen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d25d787-870a-444a-afd5-4cc09a909c33
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c4119e0-947b-43af-841b-d28be4512e30
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: p <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d65367e1-36d6-40e1-adb8-6391e7e18008
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -3LL + (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e02f5d7-b6c5-43a0-a5fa-14d585ba3ad3
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d0f18b7-7215-487f-bc99-ba83777a8ca8
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )bufsize) + (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 830d319d-f690-4d47-a148-6eab22791dc0
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 077d2b46-155c-460c-8b19-bdb62636c593
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (long long )bufsize - 2LL * (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d4b5f1c-26a4-419b-bf2d-2b2ad0869e78
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83eeb569-69e3-4dff-b4f1-28551ee0ab50
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a1dbd71-d83e-4c29-8d44-a842ced7b53d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 1 <= bufsize_0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d619d63-9fe5-4735-a9bc-d06927187c99
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: p <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cccd7120-953b-4afa-9ccb-dd09e3fe4156
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: bufsize_0 <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5901c7f0-11a7-4ff3-bb30-2e9bfd0eea56
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: -3LL + (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93e79326-8235-4413-9fdf-0720150daed8
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d27a4761-a57b-451b-9264-f8d677e388f1
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )bufsize) + (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15602505-90d2-43d2-b871-f9c3bb22d576
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d4beee8-572e-4eba-99e7-53d5de4981e7
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: (long long )bufsize - 2LL * (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d164729-e3cd-4129-95ae-f8b8f213cc76
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75a1055d-276b-4e74-be3f-d22501b53976
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 51
    column: 4
    function: main
  location_invariant:
    string: bufsize_0 != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85456b12-5177-4a0b-9874-5e5bfde7dc65
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0df6f841-5386-4390-93e9-237732d088b5
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: p <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd523d8d-ff0a-4526-ad4c-a34299112955
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: -3LL + (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9644e462-e029-4fdc-9b23-0cd5ca522935
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0e88c7c-28ee-4f17-8c14-fcbaab07a049
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )bufsize) + (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 595ebfa9-233b-4379-bd06-73a854dfd8d9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02f1a8e8-eae6-4c24-bdb5-6fd5eb41eaee
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: (long long )bufsize - 2LL * (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7c53f11-86cb-4a0f-acc5-7f53a54642a9
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 52
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7008fd4-aa6b-4d43-8ee7-5efb2aede180
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 56
    column: 0
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c66b85b7-27b2-4985-858e-228b1620aa41
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 56
    column: 0
    function: main
  location_invariant:
    string: 999999LL - (long long )bufsize >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93d6f522-10f8-48e7-9e67-c04a15b1ed21
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 56
    column: 0
    function: main
  location_invariant:
    string: 999999LL - (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e8f3460-af36-49b0-bb97-99d0035b7fba
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 56
    column: 0
    function: main
  location_invariant:
    string: ((999999000000LL - 999999LL * (long long )bufsize) - (long long )ielen)
      - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6cfe95a-442f-4081-90d4-0a94e73f61a1
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 35
    column: 31
    function: main
  location_invariant:
    string: -1000000LL + (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc41c57e-c54a-4941-98d2-6e665e9186fa
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 36
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )leader_len >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dfed262c-e1b8-4ca5-b8ce-770db2b13a60
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a6696439-9473-44c8-b63b-ae343a2a4460
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f89f3d4b-fa30-4f89-8616-6ba2bc9f15ef
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 1 <= leader_len
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f1121234-7a1b-489a-9664-a68c83dbcef2
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 1 <= bufsize_0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c8039fa-55b5-4973-ac09-afdb7951d890
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 1 <= ielen
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 02a27196-ec30-45c2-97ac-a92dfd5b5bdf
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 2 <= bufsize
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 52660a82-15d9-4db3-a16f-db34e597bff3
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: p <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c036d3cc-795c-4c21-93fc-331e515f265c
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: i <= 499999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fef1d64-4f74-49f8-8a91-ca641ac60377
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: leader_len <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06bf8b4b-5741-4cbd-b84e-262c4ce6f824
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: bufsize <= 999998
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d34a8e6-4584-4b47-9228-24e067406074
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: bufsize_0 <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a57ea924-832a-454f-9dbb-a8cd5e5b645d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: ielen <= 999999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a49cd75-fa7d-4055-8451-87d6a9058e45
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: -1LL + (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a7936d0c-3104-4756-a290-c7c1b8d32340
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: (-1LL - (long long )bufsize) + (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d6fa58f-6939-40f5-90b3-1a8215a6350d
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: 999999LL - (long long )bufsize_0 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 68f7d2ec-1441-4ab0-b860-f087c87700dd
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: (long long )bufsize - 2LL * (long long )ielen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fec62f11-21d9-4caf-b3f2-2d7525803b47
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bcdae029-9482-4bc7-87f2-0583a0406d52
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: leader_len != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27940ccc-c229-409d-a3f6-b15ba2e60706
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: bufsize != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09359f1f-e3e1-4809-a1c3-cec0aa8dc32f
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: bufsize_0 != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41ff8c6a-c6e6-4630-88b8-5f3200016e3a
    creation_time: 2023-01-27T16:29:15Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/MADWiFi-encode_ie_ok.i'''
    task:
      input_files:
      - ../plain/MADWiFi-encode_ie_ok.i
      input_file_hashes:
        ../plain/MADWiFi-encode_ie_ok.i: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/MADWiFi-encode_ie_ok.i
    file_hash: 0816346248b67d4ea9c17aaea510056f7cd51786d8081f1e3a68c606118ae1c9
    line: 49
    column: 6
    function: main
  loop_invariant:
    string: ielen != 0
    type: assertion
    format: C
