- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7556cd2-150b-4f9e-aa5a-841089324612
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 10 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e44d665-b6b4-494e-922d-77b016ef454f
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 29
    column: 8
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a10b12f5-8126-4440-964f-1e347c1297b6
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 29
    column: 8
    function: main
  location_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14dbffee-e590-4067-aaa5-250879475dc9
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 29
    column: 34
    function: main
  location_invariant:
    string: -10001LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4bbc077-5892-4714-b35d-d66804de6052
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 29
    column: 34
    function: main
  location_invariant:
    string: 9LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd9543da-bd49-467e-a85f-2f40ac903d83
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 276b071e-619a-47e9-86a0-f83621efd937
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aedee1a1-2cfd-49b8-a780-930fe46183bf
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: 10 <= m
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b97bd7f-dd12-4fb4-baab-fb010904e023
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9290dd4c-0ab9-41da-ade7-a8872e5b828f
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: -10LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acbf52b5-a2db-4645-ad74-506a986280b5
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22a837c2-ab4e-4865-9018-ce83e8619cbe
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 8
    function: main
  location_invariant:
    string: m != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cc7c888-21bc-4965-8a8e-11a6b7e78770
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 34
    function: main
  location_invariant:
    string: -10001LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8243049d-6008-45ec-807b-1bedfca5939a
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 34
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 909a8839-7d4e-4af1-8982-38c1244357d2
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 34
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cedf3d06-e96f-4d59-9567-8f54ec86f780
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 34
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b25a575-7d9c-471f-af02-0b9620e19d1b
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 34
    function: main
  location_invariant:
    string: 9LL - (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf20c627-09d2-42ac-9f4c-478739bd4f20
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 30
    column: 34
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a9d2431-f4c5-4933-a1a2-4f6872733f77
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de073bf2-2017-4b46-900c-0404851fd720
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b2b8bec-a441-4a05-a765-f784b19343b4
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: -10LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0392d384-8219-4059-aa5d-c0d0fff1e0a1
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e295e39-d1f3-41e2-b895-6aa9ea6c26df
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: ((0LL - 10LL * (long long )i) - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10e31d53-4282-4287-ac97-e362042f15aa
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb6358f1-fd2c-4f1d-8970-e12b9ff5fb0c
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 10000LL - (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c311f902-8589-46e7-a4a3-4f0931475757
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1006133-14fb-433f-9f0c-d162517e7732
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 33
    column: 5
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2d94969-0f70-428c-9f84-24f77da1661b
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bc20b64-3230-47dc-a11d-3b7ccf27f90a
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d7c4845-d7e3-4076-a3e4-d1000a57967b
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: -10LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: edb175ea-846f-453f-9f0a-313af500f3bf
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (0LL - 10LL * (long long )i) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb37acac-b63a-4918-aeea-808355e34ae5
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5de9734d-837a-487f-9e71-bb160cc357f3
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 10000LL - (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab5b18fb-aa3d-4167-aaa5-da356f912a5d
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71fe64ed-048e-46f5-84c9-133e226a8f79
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef6e1963-7a75-435e-8a47-c5a483c7e916
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -10LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 728d98ee-36ff-4fdf-b928-bf423b78844c
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (0LL - 10LL * (long long )i) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98c07925-4ca7-4edc-a9c2-0b973bffed87
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fbf35cd-f8e3-48d0-b707-9f69ef5c8b27
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 10000LL - (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8b5cf1a-8e48-46c7-92c8-78cc74021b7a
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9d90db6-d548-4f54-9ae9-5ffdd36adb9d
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 702bd8cf-f388-4f93-9284-a6823cc69a43
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: df4e241a-44d3-4ffd-8e20-80687ea28920
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 10 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e23515d9-43f4-4b95-adbd-62ddcecedc2e
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 10 <= m
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a9e3b502-6a73-4b3f-a39e-bef57630a14c
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: n <= 10000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09266fce-ba5d-4011-8a58-5cf6eae25bee
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: m <= 10000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0de96b23-5483-4d11-aa1d-0e076d27f0ea
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: i <= 10000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 542ba251-62d7-4992-891c-48ebbf1e2189
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b045a01-9bcb-4de2-8806-df805c7f4d06
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: -10LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3df99b3-2ef9-46a4-834b-93f9acbf5df6
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: (0LL - 10LL * (long long )i) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b0e492c2-71fe-45d0-8d32-ec0213c100f1
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d2630c2-fbb7-4427-aaa4-bd082cc7bc88
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 10000LL - (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7193dd5-dcf4-49bd-90d8-299259d48eb0
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c8390769-6f75-404b-8883-57019bea79e0
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ebf7cf7-474e-4a84-8b58-2eb3d5ad5b8b
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: m != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 03eaf5c2-490d-45e1-9acc-b79dc2c39af9
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 701c4876-9ff0-48d6-90c9-5abc1dcf5601
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 00daee8a-7ab3-47c6-be18-c62911e5fc16
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18b48e24-7c14-426b-b3f9-3ca59848d0e2
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 10 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ab461d7-d4d2-454f-b976-54e6dfd65ea1
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 10 <= m
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 28c01cc6-ed75-439c-bd93-e17e05eefdcb
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: n <= 10000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ff6fd5c3-5bf4-4598-a27c-f9e3df78b9b3
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: m <= 10000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e21f1238-1800-4aa8-a343-aeddf52167a6
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: i <= 9999
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 211b63c1-b6e3-4c3f-9753-dd50729ab5c1
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: j <= 10000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c050b189-2304-4073-baff-6b7894271779
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: -10LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d0a1b884-fcaf-4d58-812d-01f24b023e6b
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: -10LL + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a8b20f0-092a-45b2-8eba-2d2c56a517ff
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: (0LL - (long long )j) + (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fe8ce69-0fc6-47a1-b625-4f559ac829e1
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: ((0LL - 10LL * (long long )i) - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c28d356b-9ac5-4911-b831-c6db5493cc0c
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 10000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e5a4a5e-9777-4a33-b0b0-20edeb251755
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: 10000LL - (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 38764e8d-2584-45dc-a999-586cdf42ba35
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4739e8af-8f2e-4f06-ab90-91cf32efe717
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 26dbee3b-e714-4f79-a886-239f9aa6df09
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: n != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 021fe284-00cf-4022-8b53-746b1b71d440
    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-1.i'''
    task:
      input_files:
      - ../plain/nested-1.i
      input_file_hashes:
        ../plain/nested-1.i: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested-1.i
    file_hash: 3baf312ca85439572472b3c02ed304b3157fa97373d6ada535e5a723c6c0219a
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: m != 0
    type: assertion
    format: C
