- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32d54d6a-aba9-46f3-a39d-8e3ddd6fe7be
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 26
    column: 2
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd1f51bc-69a2-4429-bca7-ec26927c499f
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 7
    function: main
  location_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd104654-169a-4716-842b-40ecc2339620
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 7
    function: main
  location_invariant:
    string: c <= 199999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63fd6bff-809e-4f90-83a0-b59c7c6218df
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 7
    function: main
  location_invariant:
    string: (-1LL + (long long )c) + (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23b09268-79b4-44e6-b109-a58792972f89
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 7
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d978033-bbab-4616-bab9-b4c22115cd6b
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 7
    function: main
  location_invariant:
    string: 199999LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5afabe77-cb81-42af-b81c-06fabb8dd47f
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 7
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b83f8cf6-157f-4cb5-8778-3527d9f29082
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34e3bd5a-94a5-45ce-9bfd-d4fad1a59ffb
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: last <= 199999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1150108-e379-4f8d-9e72-2c6688bc6a0c
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: c <= 199999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6877850f-11e4-401f-b3a9-5687b1a13f45
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: (-1LL + (long long )c) + (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 645e4df6-422a-4615-ba59-3a4d9624bfe0
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 738bfb00-6461-40ae-8f72-6ee8ae82535b
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: 199999LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae905cff-5526-400a-a041-bf993b69bcf9
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: (long long )c - (long long )last >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb7fe81c-645c-4feb-a934-5b4e7a3717b1
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 28
    column: 18
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddab6043-8fb5-4c06-b1ed-1e1f05c49311
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 30
    column: 5
    function: main
  location_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4a391a0-3231-461a-bbca-98e4ca6b5d1d
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 30
    column: 5
    function: main
  location_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e3fece2-29cf-46a9-8e5f-300a15c81416
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 30
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73206c6b-a17a-49b6-87dc-96ce4b616e31
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 863e51f6-2402-4bc2-9b53-fbf912653137
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a10f6512-6362-4c9e-9dd6-8864bd17bf86
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 31
    column: 3
    function: main
  location_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e289dec-bc44-4a49-9038-0c8f9ec0504a
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 31
    column: 3
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 017009d1-e6bb-4ba8-908b-6b5f60bda1ab
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 31
    column: 9
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2a8479e-a34d-498b-b69c-3d9c0eb35670
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 31
    column: 9
    function: main
  location_invariant:
    string: 3 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8a69772-7692-4d85-aae2-394b18008445
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 31
    column: 9
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53b1e789-a2ad-4ef5-a459-5d06ce3205c4
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 9
    function: main
  location_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ae397ee-9e1a-4a30-ad50-81b9db4cf5ce
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 9
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 852ada39-5bce-4cf3-8586-dd2e0378e3bb
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da89ddf2-99d8-4f7f-8946-ecaea0336e76
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eccb731-4ac2-4953-b080-e44ce89e1b40
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7aeaca3-cb99-4741-b9ca-8d84f59e6d4f
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 9
    function: main
  location_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33552a5f-144a-4c19-ac79-36651775c054
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 9
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9aec19f3-9fdc-4a2f-8ad7-26b9ee41fc25
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 9
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 023fdd51-1196-4cd9-9de6-394de79ad0ae
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5645464-2d2b-4982-b636-161d559f0811
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c1d909a-424a-42c1-b32c-fcae98e4e92d
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77f19965-515a-468a-ab25-f75f98c088b9
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 32
    column: 15
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f32cf26-f444-4b85-8964-cbc3548348e6
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d7f55d9-47e8-46e4-8026-ba56da9eacaa
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 2 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9af1bef-d8b5-45cc-b657-8293876dbc5d
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc7a7bda-ae16-4baf-aaad-0fc81eb52595
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccbf3bcc-e829-47f7-bb0c-d860229b1ce8
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24838ec8-05e4-4374-a2ca-90ed3c6c3ded
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fa6356d-d2ab-4250-95cb-6b29530dbe7a
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 482526a4-90eb-49b0-a42e-22290e553289
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 610fa351-dd46-4788-bb0f-cce6ac219b98
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 33
    column: 5
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e77a2377-bdc5-40b2-9fdb-125546f4b54c
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 34
    column: 3
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9986eb4a-1196-4f6b-830e-2141a598f5db
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 34
    column: 3
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 801aeb47-77d3-4449-ad6a-af3e1f144123
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 34
    column: 3
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 886c91e9-ed1d-4b51-b3f9-65a8a50acbfd
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 942add35-fedb-447b-90e8-6d40b68fdf6b
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f503de30-beb9-480b-818b-56552e812442
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 735838ae-634d-4b61-bcca-9d27fead652e
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddcfa772-8ccf-41af-82db-265c4b8d6f92
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a82ecf4-ec96-42a1-ba42-3f74bdbcec99
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9848db30-fd7c-4e8b-9f1c-407107bbd12e
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a0dffee-0724-47ca-800d-a85f958fd84e
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4e60b6c-c1a3-45ed-8799-cc53d14a117b
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 36
    column: 10
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abc85eb8-69ce-4018-be72-6eb36f360eda
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 37
    column: 3
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec48fb32-477b-41d1-8ff6-7ed4fa3ab56e
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 37
    column: 3
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1fe65fe-6f0a-443c-b5e6-fc52e8494fbb
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 37
    column: 3
    function: main
  location_invariant:
    string: last <= 199999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77c4b2cf-46b7-45a3-bee5-eae0d2cf3d73
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 37
    column: 3
    function: main
  location_invariant:
    string: 199999LL - (long long )last >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0324b6e-cbb8-47f9-9892-7a203c2998d7
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 37
    column: 3
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43a7c487-4a59-46eb-b28b-4110987abfff
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc4a420d-552e-4b66-9245-f559bdfb1c02
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 2 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 145c51e1-3592-45ee-8b89-ba3eb43bbb94
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35b71d18-fce2-4082-b38c-4aafedb71717
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 39
    column: 5
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94c8175c-ccd6-4e99-b654-5ff87a7aa121
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 40
    column: 3
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e5aaf36-f4ee-425c-8f65-854664c53db7
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 41
    column: 3
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fa061f3-1093-448e-84bc-c78dfb772972
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 44
    column: 2
    function: main
  location_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc485616-92bd-47e3-aa4b-ad2e4030fc2b
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 44
    column: 2
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fc007108-cc5b-4b07-9b1c-8f327204836f
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3759c30a-fed4-43d4-8fe1-cd665f1ada60
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e5490201-94d0-4a51-875f-51bc90888852
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f3c82092-a408-4e28-8580-3074fdfffe63
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c02064f-f58f-4562-8756-88d379c391fd
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40ce30af-7ee8-4701-a31c-782200e9e1d4
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: c <= 200000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 36e35b0c-fd53-44a3-8e58-a6b909474f89
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 10386c82-259a-468c-8a52-34c65c482581
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: efba0a24-3ef1-445c-8af9-559dc316e947
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2f2dedc-d9b3-441e-8261-d0af7ba8aa6f
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3ac7639-94c3-4e45-9041-3d8d96b8c2a5
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 86fef345-9a8c-42b9-b39a-772f8e7caa6f
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 052e0439-e130-49df-b4de-211bb8c0876a
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bd3bd2c-cc3c-44d4-9d84-eb2ee3bc60af
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: c <= 200000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 084a977c-5f13-4e4e-8abe-21c0f6558927
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f849522f-e86e-453d-9c30-3ceada934179
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: (-1LL + (long long )c) + (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ed3d1047-2b5f-4e49-a2b0-3b794126796b
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6885da4-fb47-4ee9-b1f2-326ba4be7817
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 200000LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bea7a98e-539e-49c2-a333-65b33b6a5439
    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_delay_nd.c'''
    task:
      input_files:
      - ../plain/nested_delay_nd.c
      input_file_hashes:
        ../plain/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
