- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4f66391-2830-45fb-b49b-1904edba0ce6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca382897-3d16-43fd-8c6d-87035b2a7149
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddf6e334-00af-4851-b4ce-d6ecf61eb20b
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 33
    column: 8
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 999ef028-8d14-4d01-8627-67973394c75c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 832cd86f-3929-4dde-9477-bf4cdecd30c5
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79efea4e-1bf0-4ecb-a4df-b687463a5e0e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 33
    column: 8
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96f46d3e-dba6-41e9-8fb3-4aa49ec65ee9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 34
    column: 6
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24fcf9b7-702d-43d6-b39f-13e23538e00e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 34
    column: 6
    function: main
  location_invariant:
    string: t <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38495e00-82c3-486f-a1f3-913025e955c8
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 34
    column: 6
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b0bd3df-4a29-406e-ab6f-ab8bd787ba66
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 34
    column: 6
    function: main
  location_invariant:
    string: t != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90c4e35a-7b5a-48e5-bdef-6184b084b4d0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09bc2804-181b-412f-93b7-09d9cc719c2c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23476124-3284-4739-8e49-2e020f751fe8
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31e02b44-fca8-4a02-a83f-04d596328e41
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: t <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cad9576-d672-4102-9fa9-2a0b2726f881
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3f4b3dc-44fc-44b3-84c2-e8bb4d79ae9c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e56a4d1-dfd3-4433-bd5b-1170369cdabe
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 35
    column: 6
    function: main
  location_invariant:
    string: t != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48c52947-97cf-43f2-a0cb-65dc55d02cb6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d828ffd1-b78e-42f3-aad1-97207f66ec1d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59316c3d-62ef-40c3-bcef-3a3464ed295f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee4c3b43-f8be-40f1-9d45-1e9680b2b68d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a462039-700e-47d7-9234-5e35736d651e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 41
    column: 5
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b658753a-6ebf-40f7-b796-ddf827830a63
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 41
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e061f87-f7ad-4985-91e0-fdf2dadae73d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 41
    column: 5
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5996e521-25a8-48e7-8af6-92cb68caadc0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 42
    column: 5
    function: main
  location_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58cbafc7-07df-4d4a-b00b-1ada16611ee6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 42
    column: 5
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1554c2c4-9137-43f4-95ba-a79d9397531d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 42
    column: 5
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7e3834d-26f4-4e66-b4cb-1f516bfa0a32
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 42
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aee35efc-ef44-4c1c-b13a-25c5ecad1dde
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 42
    column: 5
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d08ba0ce-bdad-406d-a4c9-45b15f64d3f8
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 42
    column: 5
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 366f4a8e-f8d4-4cfe-9414-e3095b80f2c7
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e0d0aa3-c36e-4bc6-ba4d-fde38bcc95a4
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd2c4a37-c4d0-42a2-85c6-95302e1510b2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5757419-5243-4c39-86bd-d149f3a26bce
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13384a49-db0c-4989-bed0-42fc1400a62a
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 797422fd-b048-48b0-bbb4-403632105320
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18c4a4ff-7629-48e0-8c03-efbe2b442041
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 45
    column: 3
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa1b9b6b-9f41-40a1-a17e-1661e19434a9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 45
    column: 3
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f88c407-533e-4bb3-a68f-f0e431904260
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 45
    column: 3
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9952bdf-65b9-491d-9d8c-6804aa7f61d1
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 46
    column: 3
    function: main
  location_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a5a3ce9-f5f7-4fc8-8da4-522d30a7c80d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 46
    column: 3
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d199d6f9-6cf7-42f1-8dc5-2bc50fc118fa
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 46
    column: 3
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e32d3dbe-8713-45da-93c4-26c48fbb5bd0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 46
    column: 3
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c36df428-e06b-400b-b566-d7c5ac2b6d93
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 46
    column: 3
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 171f408e-da07-4841-9210-100f83935300
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 46
    column: 3
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e988a26-7138-4275-9736-fc14a168b7d4
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 47
    column: 2
    function: main
  location_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d345022b-0b85-4196-abaa-38ead6628450
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 47
    column: 2
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccd199c4-1000-4edf-bf70-e6abf16fea50
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 47
    column: 2
    function: main
  location_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c168456-cd7e-466f-a606-2a3ca6bb0139
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 49
    column: 8
    function: main
  location_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c55849c5-c032-42c8-b76f-5cfd9767130d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 49
    column: 8
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a298dea-84f9-4aa1-b566-7057ba8f8a54
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 49
    column: 8
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b15a684c-8e82-48f4-9f15-8bae66a3d6ae
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 49
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a6ee2b3-b2f9-4d22-aed1-b072baf907d1
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 49
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 647e1788-59ad-4397-91d5-26a800a202c2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 49
    column: 8
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aabe5f2c-f6ef-4867-ac33-5630b355a939
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 50
    column: 6
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1858c747-3351-4d0d-a4d1-42cff2ef4598
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 50
    column: 6
    function: main
  location_invariant:
    string: t <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55a5f679-9ac5-4c68-b2bb-f5ae07d9168f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 50
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 609a75ec-65ed-41cf-b338-bbe5eced4ab7
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 50
    column: 6
    function: main
  location_invariant:
    string: t != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a180f755-7fe2-4373-bd23-e0c2c220670b
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 50
    column: 6
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fe7cfb1-4b96-4e04-b960-d7c87be2be39
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c91a3e76-7f92-47ff-b065-4c53cbbd32c0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0863aaff-dcc0-4b02-929a-c1598bd25847
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6f2fb9d-3379-4374-9cb0-5016229980b6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: t <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76fd7d0d-4d6f-4f21-b037-9e4cf3b4ecbd
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2359522-daa4-4af4-8554-09182482d784
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fcac44f-ddbf-4222-9a7f-ec2b132d6fb5
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be91f012-4e8f-4295-bb50-d5ca583c9b63
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: t != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a65b86f-fd6f-4370-be98-b6bca19a6e1a
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 51
    column: 6
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0e1d8d2-58e9-4c73-b76c-34639d3e69d9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 54
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a372ec2-7c60-407a-8d70-4fe1f9beb5fe
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 54
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7a40968-812b-493a-a43a-7cd1d0ebd35d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 54
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa9f538c-4957-4a36-9343-0c764aaa65d3
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 54
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a18aab8-6eb1-471d-a5e8-50e9dba729a0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96564d16-9931-40e9-9fad-c07fba4f5458
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d617ecca-2e48-400b-ad90-87b85fe94a5b
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 400fac61-11d3-42b8-b5d1-698e94d1ae7e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3c8de55-82c9-4397-b400-18794da93d86
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76ef9bc5-ede2-4c14-b69a-2c0c9c4804ae
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e138a7e8-151a-4227-8607-68be89eb67f6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9817862-af36-427e-8705-66634bfff993
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 828fffb0-944c-4e46-bd9f-97068a46655e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 410082a4-90d7-4989-974b-4f81a2554ff2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 55
    column: 11
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d1e2864-1236-4d94-b6c5-d5fa4ac2f120
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 56
    column: 2
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba9e9531-5e4d-48d4-a2d5-33f675d4393c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 56
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 880449ff-d1d8-47ce-b1c3-da8dc1b700e2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 56
    column: 2
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f0e02cb-b0c0-497f-8f3f-be3a654fb1a6
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 56
    column: 2
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41a312fa-a0d2-4752-8366-b6e33369c108
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f27e285-824b-4e31-9d91-ef0899f8a228
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5e11848-0c0b-4273-83ac-629e611e08f9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3593f9b-b4af-4955-ae65-b5825f1f716c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26be60fb-b37f-4c7c-9fd7-3e390fda8255
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9871bcf6-a24e-4423-9750-5896c904b2c3
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5a6f9f1-33ea-427c-bfec-21e4080c2d26
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 282743a1-3918-4a14-a548-2126dcb1fdb9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 57
    column: 1
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bc7d6da-3f66-440d-b4e2-3e632237d19d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 58
    column: 8
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dfd06c7-2b18-4871-8b78-8ae6266d8841
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 58
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a57aeced-6e21-4873-acf3-3dae3c8ef5b5
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 58
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7f83081-128f-4a49-a809-051484c15cd2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 58
    column: 8
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebea3487-2945-4430-b0c5-d996851a9131
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d007ff69-334e-4513-9de6-7ab3a93f37d5
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: 2 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d813d0f2-7b86-401c-83a5-1b90415ed68e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a5c6792-b186-4a3a-8703-57a98764707c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: -2LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21b39889-1d3b-4f15-afbf-7902bd426500
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc5c4bcf-2c1b-4de4-a9fe-b03a12114eaa
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95f96297-244d-428d-b971-6668a18b813f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9f823a0-4765-4080-a915-8d7e08b29047
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 59
    column: 12
    function: main
  location_invariant:
    string: t != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1d276ab-3fe8-4566-8cf4-1011cc881083
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 60
    column: 3
    function: main
  location_invariant:
    string: 2 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e090eeb-ca88-4ef7-b6a4-c4f03fe5a33d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 60
    column: 3
    function: main
  location_invariant:
    string: t <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a75bcb5-c527-4ee6-a726-401e433b5e8f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 60
    column: 3
    function: main
  location_invariant:
    string: -2LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ceb1569-8690-49f7-bdf1-f46884cbcf43
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 60
    column: 3
    function: main
  location_invariant:
    string: t != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bb2a608-2db1-49b4-8f0a-c8341ba69776
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 60
    column: 3
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47537bcb-74aa-40bd-b3ec-800b57eb5a97
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 60
    column: 3
    function: main
  location_invariant:
    string: t != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91a3ad58-84fd-48e4-ad42-3f147c757d48
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: 2 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3836d314-2749-4fed-9e89-020462076840
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: 2 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 819a0103-a2d7-4fa5-a7c4-d819395179ed
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e588c5da-0f63-46fa-92f7-f6759380f1c3
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: t <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 903c82e3-f90b-489c-8342-3e1c137ac462
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: -2LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65497200-9363-452b-bc69-bbc1b8091fda
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0a0e18d-6e36-4544-9f29-c2cf8224c8b9
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0bdd0e2-fbfa-4909-964e-89f8cc3d52f1
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: tagbuf_len != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae2bdce6-2092-4dec-bd93-cc1349a4db7c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: t != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a19f89e9-b576-4e8d-961a-2b1e139d0e0a
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3117f263-b12c-4c87-abe6-8cb7992977aa
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 61
    column: 3
    function: main
  location_invariant:
    string: t != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e069ab1-cd6f-45f2-a2d5-a244e5302d01
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5410f9c3-c72a-426f-a3f8-38538bc940c3
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63542dbc-5fa8-4598-81c0-d30e87da6aba
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 397a2f87-3b3f-4ed9-a018-894c274d110d
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70b931a0-9995-4686-a1f8-b48f2da5f275
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8953ee4b-aa55-4498-b81a-e8559f96c273
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 504b2fed-74d0-4dfc-85f6-31cf58c7119f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7beee42-0cf4-4ec5-b815-b46bc5769c7c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: edeec643-75bf-4bae-93f3-74a10978df03
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 185aaa1f-30a6-490d-a456-6add2b265631
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 66
    column: 14
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37240ded-6a5e-4c32-8280-222b92de06d8
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 69
    column: 4
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 347c232c-215e-4b2e-8680-f8e0ff1882a0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 69
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18844822-135a-456b-a16d-094582fb1b1c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 69
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8df3898d-1e97-4cda-a0cc-c7ce9c8ee57f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 69
    column: 4
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0f6626d-2a06-4f0c-ac8e-48061bc2bc16
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fbdbbc3-f33f-45b5-bb28-5b93830fd6a1
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e184b790-ce62-4871-9585-46831fb9ef05
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f232227-f1f3-4c2a-b018-90fad8bfe09e
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e5fa365-903c-41fb-8e28-0ee83280cffe
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 180b79d3-6849-4c34-8012-0c94d63f9ba0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecd941d3-2609-418c-9380-70e3b96e554c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f13aa022-281a-41f6-9773-62deba39a25b
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 70
    column: 4
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 091ed31a-a615-44bd-af4e-5b59855f0ac0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 71
    column: 4
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 008a7677-367c-4ca2-ad5e-fd829a8b05f5
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 71
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d92fff9-7d3a-4e2f-925d-04c5c59ccbb2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 71
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2f59192-357f-40ed-98f6-914c2dce4eed
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 71
    column: 4
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d85dd4b5-cd81-407b-bc4f-641b0480a65b
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 73
    column: 2
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52d14275-0903-499d-b6ad-607c931bc4c0
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 73
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee7e242a-0fc7-474c-94be-a5ba271b5224
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 73
    column: 2
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 581f117d-1ab3-4673-aa5f-8a90917d5e99
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 73
    column: 2
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d00eb42-fb48-402d-8e90-46c733445266
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b48c5975-1c9b-4f17-83b6-efd0b0008e79
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4728730a-86ee-42b2-b741-e4590a9ebf5f
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba79f15a-7758-4c1f-a858-5ee732c07d53
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d64ade67-b5a0-4fde-b56d-c4e35831cc1c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: (-1LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6b6d456-9d4b-46a3-a877-b74125275644
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 038f4ca7-356a-4123-98f2-da7fbd142321
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12c48959-5adb-45da-8b6b-ff35ba6f800c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 74
    column: 2
    function: main
  location_invariant:
    string: t != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d44a9cb0-3176-4e90-8933-4f1fd5ff27cb
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 30
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6dea6e3-88b8-4fa0-a035-fec47f794557
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 31
    column: 2
    function: main
  location_invariant:
    string: 1 <= tagbuf_len
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1729a4c-6591-40cd-9a14-2b6bff413af2
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 31
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d11c7808-b21d-4e80-942d-9275abfb948b
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 31
    column: 2
    function: main
  location_invariant:
    string: tagbuf_len != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fcd0ee75-abe7-40bd-a5eb-5900a3db1737
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 80498a15-4a78-4802-bd9c-bf21769de919
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: 0 <= t
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 29861030-c2f4-40bb-9689-d479660f8028
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f115e416-9447-4aa7-a5f6-7c838e2f9e9c
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 150e6a16-10e6-4703-b9dd-480e3a52c743
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d813888-52e2-4f37-86a4-f8faeaa699cc
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 32
    column: 9
    function: main
  loop_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c4f6657-2bca-4054-bc17-e7efa5c983af
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 48
    column: 9
    function: main
  loop_invariant:
    string: 0 <= tagbuf_len
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f5810a27-7b00-43a9-917d-c71471bf4f41
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 48
    column: 9
    function: main
  loop_invariant:
    string: 1 <= t
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cf8981d-0fc9-4ee0-81f7-f292094ed7bd
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 48
    column: 9
    function: main
  loop_invariant:
    string: tagbuf_len <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 599b2335-7b75-4cd6-b4a8-721af6beb680
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 48
    column: 9
    function: main
  loop_invariant:
    string: -1LL + (long long )t >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cb97e34-c087-42a0-8c3d-787f8844a4c5
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 48
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )t) + (long long )tagbuf_len >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a814c6ba-2c20-4537-a53e-3c5047d40622
    creation_time: 2023-01-27T16:29:17Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/apache-get-tag.i'''
    task:
      input_files:
      - ../plain/apache-get-tag.i
      input_file_hashes:
        ../plain/apache-get-tag.i: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/apache-get-tag.i
    file_hash: ad8e21886f5f45a7c58400298498a881b4f628bf6fff913be81ab14cf250dd19
    line: 48
    column: 9
    function: main
  loop_invariant:
    string: tagbuf_len != -1
    type: assertion
    format: C
