- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a61240e-8a23-4e62-827c-c04d2604bb44
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 30
    column: 1
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cec395ce-ae73-4c0d-877e-b412d6a075ea
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 30
    column: 1
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d2afc7d-1b22-4722-a911-4c202072f471
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 30
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72d547f6-dea4-4313-9b05-16802c23eb6d
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 30
    column: 1
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1e2b5a9-1f1a-44e2-a0b6-8d3897c19773
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 31
    column: 1
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d387cf4e-430c-4683-a6a3-4394977aa1da
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 31
    column: 1
    function: main
  location_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8b720f2-57f2-44d1-9f06-c7b8582f85e0
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 31
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3db26fbf-0137-445c-8ab6-9e1759ea24c3
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 31
    column: 1
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0554608-90bd-4152-98a3-8afdd0eeadc3
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 33
    column: 6
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e40cc2e-2e0a-4c2b-8aa9-2beb49b5f4f1
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 33
    column: 6
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62420537-bd85-4c03-8a02-8d9f2d01431c
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 33
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2d40edc-11f3-44b1-b8bf-cce1c9474fdc
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 789ef6c0-6694-4400-acd6-a6d1dc672d43
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 070bbfbb-cd91-41f5-ad12-8386d61004cb
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 909829a7-34eb-4b26-8c95-d3e4cfadea3e
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ca65d29-60e6-4520-ace5-975140ed7abd
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc794bb7-8511-42c7-a260-c9a299074e08
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 36
    column: 4
    function: main
  location_invariant:
    string: j <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fd4ff92-2c01-49ba-8418-ba6518fc67aa
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 878e1635-a02d-4319-bf1d-33192f9106a0
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d198c417-9b7c-4919-aa71-1ce9e3712f9a
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a0bf9b8-c633-4cd5-b6dd-1625df88e2c1
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e81ea95-63e3-422f-a062-73bc1299915c
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3292ae9a-8b3e-4064-ba45-deae2a11e675
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cda65809-3b94-43a8-a502-a88df521865b
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )j) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bb5c93a-5ca8-4318-80b3-b0a2f34325fa
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86387383-cdaf-4d37-a630-501341cae322
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 39
    column: 0
    function: main
  location_invariant:
    string: (long long )i - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e40169d-6bdf-47ee-98ab-cb271e049c9c
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 39
    column: 0
    function: main
  location_invariant:
    string: (long long )j - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb3b7504-07fc-4e6b-a5c4-ace1fb7a1b1b
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 39
    column: 0
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b930ccc0-beaf-4752-94a4-f8d15dda1bd5
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c04c509-4786-440f-8258-c7c531399f95
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 57f43e96-5046-4646-9dcd-c4019722de8d
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f05b734-ffa6-4451-a3ab-c6750fd9fe02
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ba44132-a4f9-40dc-98cd-5293be64be7a
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c12ed74d-c7b3-4d7d-a94c-da21efbddb71
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f0c153c1-6b60-407a-8dc1-57da991a64b9
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 808ae59f-606d-4e21-85fa-36bc4b0bee2b
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: (long long )i - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21cedeec-c1ee-49ba-bc80-96460e8ff4b9
    creation_time: 2023-01-27T16:31:09Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/up.i'''
    task:
      input_files:
      - ../plain/up.i
      input_file_hashes:
        ../plain/up.i: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/up.i
    file_hash: ff5c10c83c8d29dcc2c2798035fa2754df224d2313ad9c91b6ee5bb6ca3d9a9f
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
