- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00e4f24b-fd7e-4bdc-ae51-691cec515f20
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e5cbbc8-7374-44fa-b8a8-429baadfd0dc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: 1 <= main__nlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: edf8fd51-da67-4238-8a26-e2ad167aa80a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57079846-7f6a-4f5c-8add-14959083c2af
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c51ea80-8bd2-460f-93d1-e4d0944f5765
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: 7LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d82d2b78-e1d3-43ca-960b-ea2380982ad4
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 110ef9bd-4330-4a0e-90c4-bc0b90d2f66d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  location_invariant:
    string: main__nlen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8e9f559-1e11-413c-a516-81917946bc5e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 45
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d497dc0-5e43-4012-9c05-19cd83aedf7d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 45
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f95826b8-3c58-4711-80b4-4ebe75cb61e8
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 45
    column: 1
    function: main
  location_invariant:
    string: 7LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1179475-2c37-4fed-ac61-56cb917227fc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 45
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75496d2e-2baa-4143-9233-3de4f73b7ea0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 46
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e30b9e3-816d-47a3-82ec-728f6e9cd16c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 46
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef665a38-c45d-4e96-8b44-f3e92cfb3584
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 46
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1266536e-c8e7-4019-aa3c-589a959ca933
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 53
    column: 1
    function: main
  location_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67cf2484-e4f8-46be-9b0d-3dd7489e0bdb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 53
    column: 1
    function: main
  location_invariant:
    string: main__j <= 7
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c16b64a-f967-4536-a638-212ae2eef865
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 53
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 270af12d-8d9d-4b34-92ef-6650c30fdd65
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 53
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 638a3787-4eca-4411-bc98-ee3066b94bcd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 53
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0eb60cbf-c59d-4954-bac9-766ac8a1b3aa
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1edd6ecd-a2ab-4a7f-b17c-36c1b123067e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  location_invariant:
    string: main__j <= 8
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 924b4bd9-fb5b-437f-a346-4f939faffc44
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  location_invariant:
    string: (-1LL + (long long )main__i) + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7824b36a-4160-4294-872c-a52b305da682
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2796290f-8c5e-4fcf-be79-10c15d031d30
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8ccf29a-4e95-4f1a-9093-bd0bc5e96dea
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e33ab84-7ef4-4bcb-9301-f6e55e1328fc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: 1 <= main__nlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 307a5abd-c167-4880-a5b0-e840c5d4dc8c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (-1LL + (long long )main__i) + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3294dde2-44b3-46fe-a933-7dbd283e9105
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 304f87a8-b150-4ea7-b430-c7f3efb40796
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: 7LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 190d68ac-e4f3-441e-bc24-4dfcdfc9092b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20e6ab73-9290-45e3-ba17-0c8f5b5fc66f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 59
    column: 1
    function: main
  location_invariant:
    string: main__nlen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73c77026-d656-44eb-bdfa-2a95b31904dd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 61
    column: 1
    function: main
  location_invariant:
    string: (-1LL + (long long )main__i) + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba47a408-76b6-482b-8b08-b71f5098240a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 61
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4db11cad-d53d-4579-be71-582d64da6eab
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 61
    column: 1
    function: main
  location_invariant:
    string: 7LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c09b4940-dbe5-4878-8c2b-61748eca0420
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 61
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d462e89e-5bfd-4ebe-a577-b138e93667ca
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 62
    column: 5
    function: main
  location_invariant:
    string: (-1LL + (long long )main__i) + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 635e06a1-64a0-4f35-8994-86cf761fce57
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 62
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8e9791c-89d8-45b8-ba86-3f39c0ff5540
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 62
    column: 5
    function: main
  location_invariant:
    string: 7LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f7118b3-8c57-47f2-b2a9-33e630f5a255
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 62
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6059f2fc-626d-496a-aa06-0559610d2ffa
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 75
    column: 1
    function: main
  location_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cb8d666-803d-4a40-95ff-32580b2b7ab9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 75
    column: 1
    function: main
  location_invariant:
    string: -8LL + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d06003d-f578-4d9c-8973-0945d3101459
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 75
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4913c8f-345d-4c96-bc5f-cbb547a0d553
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 75
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 709f5c04-6030-434a-b191-8fb8d6d75cca
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 76
    column: 5
    function: main
  location_invariant:
    string: 1 <= main__nlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9df19ff6-4656-4c19-a5fe-af260e0e59dc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 76
    column: 5
    function: main
  location_invariant:
    string: 1 <= main__i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cf101ac-34d8-417a-a58e-cedc94cf7481
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 76
    column: 5
    function: main
  location_invariant:
    string: -8LL + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e5db825-14d4-4812-aff8-ee68e869bdd5
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 76
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1172cfb-6aa0-426e-9689-ff65ea28162b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 76
    column: 5
    function: main
  location_invariant:
    string: (0LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f942d0e2-1a15-4834-b6bb-9cca1fcbf987
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 76
    column: 5
    function: main
  location_invariant:
    string: main__nlen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09c57210-2cb4-47ef-b509-6437c2846b2c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 78
    column: 1
    function: main
  location_invariant:
    string: -8LL + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0235d8d-540d-4875-b64d-5b645fbd5608
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 78
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1943adf-713f-43f6-9733-0bd499f94b4e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 78
    column: 1
    function: main
  location_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98876149-5231-44bd-a187-dd70cbff8641
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 83
    column: 2
    function: main
  location_invariant:
    string: -8LL + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92673382-4c89-4f83-afca-6b1dd19f423e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 83
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7eca25fe-a200-4334-99ac-a4d8917413ea
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 84
    column: 1
    function: main
  location_invariant:
    string: -8LL + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8379c3f9-0bc9-431b-bd2a-64231872879e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 84
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db1d927c-5835-45f5-ade2-db3ce22acae0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 100
    column: 1
    function: main
  location_invariant:
    string: 0LL - (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b65960a-a90e-45e4-9369-2e681c758d6f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 25
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4366217a-f201-4aae-bbdb-302c72067cf6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 26
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84849088-8248-44b1-8607-2644ea361259
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 30
    column: 1
    function: main
  location_invariant:
    string: 1 <= main__nlen
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c03f699-f6d9-4df3-88ac-64676e293dbe
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 30
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec0d930c-ced0-4e67-aa59-247c89216a20
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 30
    column: 1
    function: main
  location_invariant:
    string: main__nlen != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 763323a9-8fd1-4879-ac8c-40b67cd59730
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 32
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d6880b6-b7c7-4eb7-9630-ec46352eeb5d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 33
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21d723c8-b2aa-440e-b9bd-6dc6acd07cb0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e9c0ee7b-2791-4dc0-8d2e-ed80999a56d4
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 92d2863c-0fbf-409e-bb20-3e21c5d6f10c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: 1 <= main__nlen
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fedb9662-66c8-4aef-bcb0-ac913b4f596a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: main__j <= 7
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b085e686-dc31-4d96-abf9-ffe7a8b54dec
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f09641dc-5a82-4069-9993-f8eea2f2b72b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: (long long )main__i + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 74e2c5b3-596c-457a-8aba-d055a7a4c905
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: 7LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d6b37f70-b7c8-4f72-b5d4-f5369d16bb57
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ce2ff9d-a057-49ae-aa68-e316aa5f96e5
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 43
    column: 1
    function: main
  loop_invariant:
    string: main__nlen != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b4035a3-6b68-4ad1-97f2-08a92d82216c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b7d2c069-3dae-4742-840d-1ef02e2ec706
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ec3e9ba-49ec-48ee-8917-f02e40c96053
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: 1 <= main__nlen
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a0ece5e1-0957-4f79-8388-5914546ba77b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: main__j <= 8
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 50d81a12-c33e-4af3-bbd7-06a299cc24aa
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: (-1LL + (long long )main__i) + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b93336b3-48c8-498e-b651-0448a4325814
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 426b0deb-1c67-4426-8665-68cc9bbef419
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1303b18b-2d43-4ece-b1d0-a62ab010ad5a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/id_build.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/id_build.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/id_build.i.v+lhb-reducer.c: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/id_build.i.v+lhb-reducer.c
    file_hash: 2f03a9521f9986f7627623e3bf6c079dbfbe3dc9d9c229ed8d14a2828a7d6850
    line: 55
    column: 5
    function: main
  loop_invariant:
    string: main__nlen != 0
    type: assertion
    format: C
