- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1dfa3a55-bd2e-4789-b718-b947f29020d6
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 268435454LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 306e87da-4b54-4a13-aa11-6e88e3ef03c6
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 25
    column: 3
    function: main
  location_invariant:
    string: z <= 268435454U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0324c498-df06-41c0-aa62-f7f99221bba3
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 25
    column: 3
    function: main
  location_invariant:
    string: 268435454LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09c01eb2-e61a-46c3-809c-f22b3be42e2c
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 25
    column: 3
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 190ffcba-71a5-4477-97d3-b5a5ddb5f474
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 28
    column: 1
    function: main
  location_invariant:
    string: y <= 268435454U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ebc93b5-e602-4712-bcc3-70ef25fb1f57
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 30
    column: 4
    function: main
  location_invariant:
    string: -268435455LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33aa3bae-f1e0-4b54-befd-a64b7f38de3c
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: x <= 268435454U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8a25a36-5b00-4cb8-9c90-93502d11922d
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 32
    column: 4
    function: main
  location_invariant:
    string: -268435455LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 841a3a20-d46a-446e-94ba-38bd408ef232
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 34
    column: 2
    function: main
  location_invariant:
    string: -268435455LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 470e1a3d-4722-4ba8-a35f-e48e83b2a3da
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 34
    column: 2
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2063267b-61a8-402e-ba3b-de6d5b9ef746
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 35
    column: 2
    function: main
  location_invariant:
    string: -268435455LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 056f6e84-79c2-4547-beff-bb66b50128fc
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 35
    column: 2
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cc5a512-f68f-47b4-b602-4fdbe0965e45
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f460b738-8261-470b-96be-f7a523b50dd1
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bed853d-0155-4ce3-a570-5da1f51cf16c
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 074208f7-7fbf-4db9-821a-d8653d9a80f8
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d49631d6-4929-4e87-9d24-192561d98ab2
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24f1ccb0-604f-41cf-8476-699d7ef43df2
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb9ed56c-20a6-4bc8-a486-23fa2f60680e
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e55f4b26-3522-439c-bb3c-9aabfe859356
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60dfb4c3-34a8-4bf6-8060-3974f40f56d0
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24d00072-a3b0-432a-b8bb-9d2976764784
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9767545a-10f4-412e-ac49-e5fed91a5f5d
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd776235-e75c-405f-a763-9ea35700f0c3
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2853acf6-2037-426c-82de-9d6faad80b01
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03fc8318-61a0-4d17-88a6-7f3e32b7916b
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a198c949-5f74-407b-ae4f-80659ed3f9ec
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2867ece5-192a-44fb-90c7-c95a1c77be28
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7775f83f-c8a3-4227-9687-5dafc7d924cc
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25fc2956-9808-4a0f-946e-804a93fe0966
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e523515f-88ce-4877-bd5d-d10fdd23fc00
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ce0afd9-302c-4a0e-bdc2-d97d9a8f8d02
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )w >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c03b610c-3c7a-447f-991a-12b2c5f6ac22
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 20
    column: 4
    function: main
  location_invariant:
    string: y <= 268435455U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88544a7a-77e0-411d-b163-0ff9a1e4b179
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 20
    column: 4
    function: main
  location_invariant:
    string: 268435454LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80a095a4-5c55-498b-8a2b-42d9de5da98b
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 20
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 561fbc1c-1d61-4dc3-ac76-a68a18595094
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 22
    column: 11
    function: main
  loop_invariant:
    string: x <= 268435454U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 156282eb-84f1-4272-a12e-4eb58f88a048
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 22
    column: 11
    function: main
  loop_invariant:
    string: y <= 268435455U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a59963d5-3f24-4f45-b880-ac7d60ad5e87
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 24
    column: 8
    function: main
  loop_invariant:
    string: x <= 268435454U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4695ea7-558b-4aff-9503-44c7368952ee
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 24
    column: 8
    function: main
  loop_invariant:
    string: y <= 268435454U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f98f7b6-1cee-44a6-a8fe-3dda2ae9386e
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 24
    column: 8
    function: main
  loop_invariant:
    string: z <= 268435455U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e175f5c3-389e-44a9-adca-d5d9be40e244
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 24
    column: 8
    function: main
  loop_invariant:
    string: 268435455LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8af30a9-a78a-4585-ab7a-32c853ca7919
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 24
    column: 8
    function: main
  loop_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b374a9f1-92ae-49fb-b046-cbddc8dd4c92
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 19
    column: 9
    function: main
  loop_invariant:
    string: x <= 268435455U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b84e5b3-d5dd-4b48-b85a-36ec45a32383
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 19
    column: 9
    function: main
  loop_invariant:
    string: y <= 268435455U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f7dbcf36-e13e-47ac-8bb8-9af0a52872b0
    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/nested3-1.c'''
    task:
      input_files:
      - ../plain/nested3-1.c
      input_file_hashes:
        ../plain/nested3-1.c: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested3-1.c
    file_hash: ed8e064f31e82b4c33cb383334d25637eef982ae8d5b8603579b97c7fdfe808e
    line: 19
    column: 9
    function: main
  loop_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
