- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12f7f524-c5db-4ef1-b7b3-b8a9d6f54632
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8389356f-d594-4882-b8be-2f127c02254b
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 995741cb-ce71-4e5a-a9c5-ed1be4fabe0b
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ed031ed-bfda-4a42-8193-ae5436b2ba0f
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0595998-ef22-4a9d-b8ab-c77e5770836b
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce14cb57-7fb0-4ad3-bb5d-c7b3c3e54912
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a1f8d8e-918c-413f-9e2a-2c5b14107f8f
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f6485aa-9ace-4a70-8312-2a2c9b5c2170
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f094718-822d-4394-90a7-38600652ee50
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd10aeda-24b7-4103-a51e-722f56c20099
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44660f3b-5a70-4909-b1ed-336ca972cd4b
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0625e09-daa6-4141-a233-698a34bd08f6
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d59b4aad-f421-412c-a950-bc50a62e985f
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01e770fb-32f7-4bf8-845f-bc76f624cea6
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8340a71f-c921-455a-b415-dce1ddea0916
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7aa5852-00d1-435b-8ad0-7e7e75e2b7c1
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cfad6186-e5bf-4509-95b8-37afb019c3bb
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 236b3336-f4ea-4739-9f04-d3944779f8c3
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 095afd7c-3619-461e-9407-4c6aeb188216
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2680602-699e-4d97-bcda-2f69660e6a47
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 87b70b55-655e-4130-8ae7-93936b9ee576
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: c <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 527c051e-05c9-4163-95ed-04d879f153c1
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 722489d8-8708-4dd6-a818-299fecf4b0a6
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b57d2c8-5f55-4a6e-9144-a77baa012ca7
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04ab5df7-8cf4-4b76-ba96-d587fd702a92
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e574bdf-3128-4042-827e-7a77b81a757c
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 25
    column: 6
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5df27cca-b7dc-4ab3-bb35-dd995c76492d
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: af24e3d6-61c5-4b21-97bd-00049e1ea435
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a2cbc97-1874-410e-ac8c-db6360a294b0
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be008f02-8eeb-40dc-8e66-a1db2fc002c1
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f30f3f08-14fc-4380-b867-24f3fce3f744
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be49825b-bca9-4c14-9a19-bcc5e918572f
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b6f8097b-f745-4e33-9fa5-e181afcedc1d
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: c <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b751528d-aceb-4398-937a-eebaa9f5ab44
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: d <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a8d4b5f-8c11-44fd-b35c-1b8736dd9807
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b35b3fa8-8d83-4b6d-ab24-c16a64121ac2
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d18f1ca-4167-4e4b-8692-76e81f3f5f79
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a37128d-015f-4d09-98f2-869875322017
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fb537f79-5acf-44a5-b5b4-4650430023e5
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 26
    column: 7
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a4abb3e-6ac6-4fa5-9038-c706db903a5a
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c453f44-1b37-483a-92f3-b2d18cdb91f7
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 94171abc-6f3b-4444-b3f5-a74f21a55ea9
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d10bb972-d49a-48e3-895a-23227c8f3a4f
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1972f2be-2e58-41c9-bda6-409ea1556993
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 0 <= e
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8683497-006b-450a-98d5-bd4d5e3c0b88
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c7293c7-d6cc-4822-b2c7-e1446fa4a4e2
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: b <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ddb51601-d3c2-4cbc-a33f-f8b457c5f04e
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: c <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 910f7471-5981-4a04-aa02-b23715e7a49a
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: d <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b9e0b954-0d18-4b77-b1c6-2175d0554693
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: e <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25a35a94-ccc1-437d-b6e3-9e22ea40d786
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: 6LL - (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e1ddecf9-d2fa-4644-9639-321bb04e8ab8
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 67cdefa4-8dca-44fa-bbc9-7ffa53bdd466
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26fa858b-2552-435e-90c8-6a04619d0101
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cf5acb0f-e40e-4758-a3b4-a43b7e417164
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b20c8077-0f12-4c2b-b8b4-58156877e663
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 27
    column: 8
    function: main
  loop_invariant:
    string: (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 11fca5ba-a3c5-489a-8ca1-7fbd41db3472
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 29f930b4-b4b9-4d34-999a-dc89a8d6d592
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: a <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 546e2a76-a0b2-4151-98cd-c2a72145f9a2
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 62769ba2-5307-439c-be27-0480dd51bafb
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bde12618-68e3-467e-88aa-30d284fa9a11
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a5071d3f-d941-47dd-82f2-b0509e99e1ee
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d14174fb-cea0-4109-bedd-f7b251ce5bfa
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 23
    column: 4
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a13fe1e7-86fb-479b-b97e-392cee995f0f
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 078d40d6-937c-4bcc-8268-1d6e2e60b322
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cbfd9a66-5aaa-4aeb-a607-accda545e741
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: a <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7508ab2e-f138-424f-af1c-3c8a12a8b3e8
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: b <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b60d5953-abe2-48db-937a-c192348c8510
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: -6LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 11e8457b-f62d-4133-9b69-7d8e85ce86e4
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: -6LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b368190f-e093-4944-8054-be4ba07e1491
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: -6LL + (long long )e >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c28599aa-e047-4f59-a9bb-8069466f1f2a
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6104d9ce-657e-46e0-a204-dbbd8ca66bb7
    creation_time: 2023-01-27T16:29:45Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/nested_5.c'''
    task:
      input_files:
      - ../plain/nested_5.c
      input_file_hashes:
        ../plain/nested_5.c: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_5.c
    file_hash: 3d0f32d2f39934bb8fd732fa206acfa5d2fb4cacaee37919c0e4326d55891c86
    line: 24
    column: 5
    function: main
  loop_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
