- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b190ff7-c7e8-4638-b898-d106ddc3a627
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  location_invariant:
    string: 67 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6419c2b5-a030-4514-b676-8cae72dbae0c
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  location_invariant:
    string: 67 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 870e1cf7-786e-4dc5-b745-d774dfcd6c73
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  location_invariant:
    string: main__x <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5579ecb2-0c15-4d6b-9a6c-2de59f333075
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  location_invariant:
    string: main__y <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4c27dc9-fd08-4c99-b41a-62eaf3ab1d47
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  location_invariant:
    string: -67LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f9cba01-bd64-4bde-aacf-afed947806b5
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 422
    column: 5
    function: main
  location_invariant:
    string: 67 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b5a7260-ef0e-4d7b-9eb1-c18977e856a8
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 422
    column: 5
    function: main
  location_invariant:
    string: main__x <= 99
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee485d1f-ede4-489e-a581-0055ec9c7e74
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 422
    column: 5
    function: main
  location_invariant:
    string: -67LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d16f60a5-13c8-4cdd-a3ff-2d64e8185147
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 422
    column: 5
    function: main
  location_invariant:
    string: 99LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 828d787b-1f7b-4030-835e-6787dd1643e3
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 422
    column: 5
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb186926-5dda-4830-8d51-b766dff66ae4
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 430
    column: 1
    function: main
  location_invariant:
    string: 67 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b960db9b-64a3-4a25-8455-36eaac7398bc
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 430
    column: 1
    function: main
  location_invariant:
    string: main__x <= 99
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85ce6e12-fba2-4c6f-8365-9b25249d2984
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 430
    column: 1
    function: main
  location_invariant:
    string: -67LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: deb69cd7-c1cb-46fd-9032-bc0961cec55f
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 430
    column: 1
    function: main
  location_invariant:
    string: 99LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ceed6f7d-7c75-4a0b-b680-f5d49f61885d
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 430
    column: 1
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 360aef51-8b81-4dfe-9439-dd1552139324
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: 67 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d97fd8ef-d5cd-4cf1-832c-8a1be62f6c94
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: 68 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa3e271f-50ea-4f0f-8916-65c3cc1e2f55
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: main__x <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a05e598-bb53-419e-a17c-a3b551388998
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: main__y <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8f3b189-ca64-42a3-b9c1-f9661bd553a8
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: -68LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fede439-0deb-4fae-bdda-dcaa5d0c2283
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: 100LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b767960-67c9-4287-8bdc-386a19d49036
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 431
    column: 1
    function: main
  location_invariant:
    string: main__x != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4385be67-e47b-4916-812b-04dbd9fda6a2
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 439
    column: 1
    function: main
  location_invariant:
    string: 67 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 056312b6-39ca-478d-a3b5-85403a02f250
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 439
    column: 1
    function: main
  location_invariant:
    string: main__y <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b0c9156-c7b0-478d-a2ee-0fb9dd718ab1
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 439
    column: 1
    function: main
  location_invariant:
    string: -100LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a869058-7027-4499-994a-5a7a615bf078
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 441
    column: 1
    function: main
  location_invariant:
    string: -100LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7db22eae-7866-402d-b447-c8b22cf04482
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 442
    column: 5
    function: main
  location_invariant:
    string: -100LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f002586c-4c47-4250-9694-539dc268d1ad
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 449
    column: 2
    function: main
  location_invariant:
    string: -100LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3775ef53-d5a8-4672-a2fa-e0eff722172f
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 450
    column: 1
    function: main
  location_invariant:
    string: -100LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 20a89c95-1e66-4044-b9b6-6d2d07bec7d2
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  loop_invariant:
    string: 67 <= main__x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ee4422a3-d6f5-4f15-9189-aa000ae51786
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  loop_invariant:
    string: 67 <= main__y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e09e8990-937b-4c08-824b-0452a866ade4
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  loop_invariant:
    string: main__x <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 51ef5ee6-19f8-4730-9b55-9fac609c4463
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  loop_invariant:
    string: main__y <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9407ae5b-e7d3-4a82-b377-4b2a6e514365
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007.c.i.p+nlh-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+nlh-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+nlh-reducer.c: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+nlh-reducer.c
    file_hash: 78a4cc43ce1234c075e2c73cca2f6f44edddfccbee7278c746f2db07d17136bf
    line: 420
    column: 5
    function: main
  loop_invariant:
    string: -67LL + (long long )main__x >= 0LL
    type: assertion
    format: C
