- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad094a32-3af3-4dbb-9d13-78d7ecb0891c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: i <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65765e8e-1cfb-4800-9ece-57bc24c59b75
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0391deb8-91ab-43eb-a8e7-3f17d7058be1
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd4a4ea7-e437-4a4c-841d-8c4ad689d8a6
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b689193f-fbac-470c-8811-7481dad54216
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8fa8b6f-89e2-45de-9eed-be4d1deaf5f8
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41a92dfb-8305-49eb-a1d9-00f3b5c30f29
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7e17757-81f5-4ed5-a4bb-429e1955585b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72eef368-9de2-47dc-b6c1-676f59165e65
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7fe1b2b-6ea9-490d-afd4-526f6ad950d2
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 170dee32-0985-4e28-bb14-87e1294e0056
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea1f77e4-347f-4d24-839d-5aa7da6fce39
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: -5LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f6fe0c3-c528-4d0a-9752-5da4fec5832b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fba6ca0-7323-4d56-a769-35f0924832fb
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04a6ae14-d32b-49b6-9cba-6e2698f14600
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17efff33-fac8-4733-b27f-1d93ae28c580
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7cc7994-96d0-4203-adf7-43853171ca22
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53ff25d1-a37c-4cdf-9e0e-8016531eab03
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b11b3eb7-f0d5-458a-a181-6b9e6bb2f959
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 001a5082-574f-4667-8335-8bbfc24b42f8
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21faf943-1458-482e-98a7-7e2f2548796a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: -5LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 470d2e4c-f884-4768-b30e-5032a96ba804
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8a07df1-01f9-44b9-9633-2bacd1b35c6b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e92b030-c54e-4cd2-83f5-d9910d46a57e
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abbd6a57-8f61-4afc-9d59-0b7814b4d966
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1400d500-ed7b-413a-b212-bea4cd7c12c3
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4de72e49-f4c2-4b6d-9a93-75ba55a7fda5
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d3759e4-a3fe-4a61-b4ef-c8f33fc102cc
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc03477f-44fa-45c1-a310-79ce86495ed5
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 35
    column: 35
    function: main
  location_invariant:
    string: (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b8775eb-8286-41ca-ad46-ba5d618c8e67
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: -5LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c198ca34-15ba-48bd-adc4-eca11c57c10c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9608a6b-142d-4f22-b994-fa6437060a38
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd0b99c-dfb3-46ba-af02-13923ce1775a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b946cc60-3952-4c96-81d7-2909c17c47ab
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d5eec32-c995-4552-b93a-d4551ebf7805
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10931c5d-16d7-48dd-bedc-91405b6e23c8
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a56741d1-8546-4957-bb27-78769269bedf
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bf4114d-554d-4fcb-89a7-a2d3e9a151dd
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 786fb54e-74b8-4217-8bcf-7cb542d4a508
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: -5LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 575e0f1e-8bc6-4f30-af4a-cb565e734996
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53326e28-e172-400e-b310-509c9b60dc85
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 429e8e40-a8d6-4808-86db-c386f9e81868
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b29a721-7c6e-490f-b31a-41d15e7e8dca
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04b09ca2-d3c5-49fa-ae57-6061e4834a44
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe2321de-a807-4fe4-a34b-e22d90f90cee
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 39
    column: 4
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf660987-27a5-406c-99c5-9a72688abb63
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: -5LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51294ba4-4845-49ea-afbd-04536bbed063
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84ed6c0f-24d5-4c8a-b4cf-4e6a6d2d2cd9
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 225c636d-7ef4-41f0-9323-11ea03e3303c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 063a7b63-2455-4bb4-a5a2-42a49a3414ed
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94a2790f-afe7-4605-bef3-d23caa558426
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67203bff-477c-4b9e-b337-f5f460fb4fee
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 41
    column: 2
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0602c6ad-d121-45af-b023-096bb7ed5ad3
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d28c24a9-69db-4525-803e-16572ecd0938
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: j <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c8968d0-2f29-4c5a-a0d6-545808952d48
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d60f4df-e282-4658-af70-37dd323cc088
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: 1LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e653aa1b-ca1e-4f6f-8074-82825b5df30d
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb4f7317-6980-4bfc-9a05-81eaa2b3d0c4
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9db220f-269b-493d-99a1-702191369790
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 44
    column: 11
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d2f7347-0b19-4da2-b88d-ec0d42f9916a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e726ea2-adbd-4476-81d2-6b0d718963f5
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: j <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0eac649-0fdc-43f9-b5d5-55941a8d6459
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ea93cd0-9b26-45a2-8301-1464d57de149
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: 1LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0310538a-2195-47ce-8b8c-8970bd6e2f76
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7519d94-45fe-4234-b964-b17ecf3d24c9
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf19225b-5f9c-4c91-9de1-6dec95812e8a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 45
    column: 11
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4ca94e2-54f1-42f1-a31d-f54005a8d5f9
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 47
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d49e0dc-b4e5-45b8-8483-5e8531b39228
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 47
    column: 2
    function: main
  location_invariant:
    string: (long long )i - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36a9d758-12bd-4dc1-bfa1-a795a4c7419a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 47
    column: 2
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8253616-36ee-40bb-b1c2-05ff1dc0f84d
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 48
    column: 6
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aca53600-5db6-4352-9bd3-ea43a6aa0e3a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 48
    column: 6
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 243b9877-c7df-4dd1-9e31-089b52f75d8b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: 0 <= cont_aux
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01750dfc-d970-43c5-a82a-477d3882be5e
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: j <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14a3c71f-e506-437f-b8b6-f91d59dc837b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: 1LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92386db7-ca6c-4f23-a99f-463d5f16cc1a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5eb932d-6b34-4e3e-ba9a-9f3892433de7
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3674a01-05d3-4d9f-813e-2435696c6330
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c904731f-9089-4457-81e5-d42937b0754c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 53
    column: 11
    function: main
  location_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0d497c7-29f3-49b6-a75d-cf515cfa1461
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: 0 <= cont_aux
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e307e46a-b584-4efd-8286-ae0e5bc16bf3
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: j <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38a1fca8-6e5b-435a-b08d-720dbd0631ad
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: 1LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80c0c106-494a-498c-ba3e-1f9a404a42cc
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7922821c-2f2a-40df-ab36-db2d911b91f4
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 66a5feb6-dee3-4bf0-8cba-d0ce1d57d695
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79ef49ce-b99e-432a-b2e0-ecd4b6abdcd7
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 54
    column: 11
    function: main
  location_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af99098b-d250-4da1-a754-cb2ee6c4ed75
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 56
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62df665a-0c31-4acb-8d08-fb7d1fb63aa4
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 56
    column: 4
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3148987-c594-45a5-aa87-6eb4a78b0871
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 56
    column: 4
    function: main
  location_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fd19486-b20b-4773-a114-ff0d6e8b9ddd
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 58
    column: 2
    function: main
  location_invariant:
    string: 0 <= cont_aux
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31c9bb41-cff1-495b-b33c-b33c17cbe97e
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 58
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb9da0ee-a4ce-49ca-a640-4d433bae4caa
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 58
    column: 2
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1979bd50-0865-45cd-bd5f-c3a811d25693
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 58
    column: 2
    function: main
  location_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78360e74-28b1-45eb-a44a-50514945bfeb
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 60
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aac672df-43b3-4451-91fc-6fe0188a439c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 60
    column: 2
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71163ad2-af78-447c-836d-dc383256d903
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 60
    column: 2
    function: main
  location_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09cde710-835a-4174-8caf-de1ef35e15ef
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: 4294967295LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f18fd48-70f1-4fa0-91f9-99ed26122ab1
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c089e568-85ee-411d-9311-603b7f79c8b5
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fa88c0d-fca2-4224-80b0-1f99f2db53ba
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cabc6c47-797e-4f42-b658-b2616afb66f6
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82656bbe-e52b-4f14-a8ec-2bbb84a72bb1
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93a1e803-72b6-4ce9-a7c3-a7c7ea8c659d
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 276849f1-2062-4d1b-8dd0-b4560b6c3eba
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98e7083e-b296-4861-a6d0-3e6f5aa5e76a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 767c35f4-eb3f-4766-a4f8-120fc9a9f48e
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 30
    column: 24
    function: main
  location_invariant:
    string: (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bed0ba92-6ce5-44c4-83e6-5a668a082f6e
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: i <= 5U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ec30f92-e8c5-4030-9c95-0a23df8ad773
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b7c946e2-11da-41ab-9e6b-50d5eab9f89b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2627c38f-ed37-4d05-8032-c2444f2e27c1
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c62a29c-e3ab-4662-9862-b6f6c21acc14
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a927bece-f5b3-4a4d-8d44-f2ca620e70bf
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 79f4f677-b6e6-4092-ad58-11826b02a23b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ba0f2c83-35c6-4e8c-b8ac-6d0080979c7c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09dc7c9e-eaa8-43ff-8fe1-8efc76bc0ba5
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 82839058-d959-4501-93be-76678c6725ba
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 33
    column: 5
    function: main
  loop_invariant:
    string: (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 923d645b-4ee2-4910-9adc-be662b60e751
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: -5LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 82e5e039-94a3-4293-bedc-0ebecefafcd0
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d782e113-ddbc-4ab5-bc4b-f1b8379c5adf
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e05999c-2106-4f27-9da1-164d9727ea1b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4a32ba2-c9b4-47a3-841c-6b5c31bd2338
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 60077209-673c-40c6-ae3b-10ea80913ea1
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: (long long )cont >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cce13d65-3318-47a6-b792-d4e23ecdc9ea
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 38
    column: 8
    function: main
  loop_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c469de9-9bc7-49bd-8fec-b41848116a0a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 42
    column: 5
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8e07d73-b8a7-47a3-a389-2abacb8856b4
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 42
    column: 5
    function: main
  loop_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 66bbb2fd-ef41-4794-be03-951118d3643c
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: 1U <= n_caracter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 709faf26-7d85-47aa-8b87-2b0da9d281eb
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: i <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: af754faf-5554-4626-9a43-fb446770cdd2
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: j <= 2U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4866ef4-75e1-40f1-b50f-274661cfcb0f
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: (-1LL - (long long )i) + (long long )n_caracter >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a46d1362-235a-4e94-a6e7-b86124516527
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: 2LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b10fe633-0284-479c-b459-beff2052ace7
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b58301f-8567-409e-bb0c-adf134524650
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ca436979-06ec-49f7-85b8-958d08bd444a
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 44cd7a2d-a967-416c-aee8-280d82c80652
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 43
    column: 8
    function: main
  loop_invariant:
    string: n_caracter != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a19d5c1-2236-45ae-9062-960f5838ad6b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 49
    column: 8
    function: main
  loop_invariant:
    string: 0 <= cont_aux
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ff09c1c-26bb-4714-b1ad-844db341aad8
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 49
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dfe2f997-ff27-45be-8605-19b17191685d
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 49
    column: 8
    function: main
  loop_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18875758-d5b5-47ce-bb0c-93a0b57f7120
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 49
    column: 8
    function: main
  loop_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 00c60d7e-99bd-4ea4-9449-e742200650db
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: 0 <= cont_aux
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dd1ce38-435c-4218-96b9-8ec849f8dd91
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: j <= 2U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c2bfb57f-3c2f-4e48-ab0a-ef1387e7877f
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: 2LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 647b029f-f220-46a2-bc7f-7911ced6049b
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d53086e6-6761-441a-800c-d5af3a6b0ec2
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46a1b27d-8d43-4b4d-9d8e-4b511550fdff
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: (long long )tam_string >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5ed093d-6f75-43f9-8c81-e6c3cbaf5e72
    creation_time: 2023-01-27T16:31:11Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/vogal-1.i'''
    task:
      input_files:
      - ../plain/vogal-1.i
      input_file_hashes:
        ../plain/vogal-1.i: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/vogal-1.i
    file_hash: 0004a4c1c8347096eaba7e87038be30bb20b14d3b5abd082e79b4b4e835a243e
    line: 51
    column: 7
    function: main
  loop_invariant:
    string: (long long )cont_aux >= 0LL
    type: assertion
    format: C
