- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35999404-fa45-4029-8202-bcfd98c12987
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 40
    column: 5
    function: main
  location_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 534694af-11a1-4c93-bd25-fcf6b5196a2e
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 42
    column: 1
    function: main
  location_invariant:
    string: -998 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2dd5b43-619e-453e-b29c-06afc71d3ec0
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 42
    column: 1
    function: main
  location_invariant:
    string: main__x <= -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a30e6128-8879-4986-a0ad-0057b3a9d7d6
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 42
    column: 1
    function: main
  location_invariant:
    string: -1LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01471ae4-7da7-4ae7-8a21-3915012329e8
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 42
    column: 1
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5129283d-e840-48c8-98df-b5156df1b449
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 43
    column: 5
    function: main
  location_invariant:
    string: -998 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b765bfd4-2ee7-4fd6-a93e-3744b1f686ee
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 43
    column: 5
    function: main
  location_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1f3bd72-6337-42ea-a223-c844cb9ccde4
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 44
    column: 1
    function: main
  location_invariant:
    string: -998 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9cdcae7-0cc4-4035-badc-0aad5271ee6d
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 45
    column: 1
    function: main
  location_invariant:
    string: -997 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 841de8bd-4718-4b6f-8209-79ba1cf00d40
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 52
    column: 1
    function: main
  location_invariant:
    string: -998 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c194e67d-0a6d-4f85-ae42-9ce2b4931312
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 52
    column: 1
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57818c5d-236e-4265-aaea-fcb478773ef4
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 54
    column: 1
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff8fea58-7760-4961-ad54-e3c6f450c3df
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 55
    column: 5
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68ccec02-555c-4a99-84ff-3d96ebe56c8b
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 57
    column: 2
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79f3eef5-5544-4b7d-80ba-c4848fb48729
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 58
    column: 1
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2b42c75-9b8f-4f9f-b569-518a0a9cf804
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 62
    column: 2
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5569bdea-7c27-4941-b8ea-2286af8d83fe
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 63
    column: 1
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc77971a-b073-461f-ab62-a5a59bf33667
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 22
    column: 1
    function: main
  location_invariant:
    string: -1000LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9e74b7a-f321-4d53-9c9b-28bc1f8095d9
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 26
    column: 5
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74ad595f-d9b0-4a2a-b431-674052af8259
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 26
    column: 5
    function: main
  location_invariant:
    string: 999LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0aa9f321-3b07-4f63-bd5f-bd38d7b493cf
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 28
    column: 1
    function: main
  location_invariant:
    string: -1000000LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58bef164-bf99-4f07-8ede-2b9c1ee5a81c
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 32
    column: 5
    function: main
  location_invariant:
    string: 999LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c8674b1-8c2b-4a5a-b467-24eb629ab1a3
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 32
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 758ed410-eff7-4091-8404-57fc56f67f7b
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 34
    column: 1
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a233f518-3da8-4915-b1f3-5fd5860e36ab
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 34
    column: 1
    function: main
  location_invariant:
    string: main__y <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdcccd5c-039e-40dc-ab93-75bbc01bd07b
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 34
    column: 1
    function: main
  location_invariant:
    string: 999LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c0e2584-4483-40a6-84a4-58e8695918dc
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 34
    column: 1
    function: main
  location_invariant:
    string: 999999LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1380746-3b19-49c1-a7a9-bc948db9331d
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 35
    column: 5
    function: main
  location_invariant:
    string: -1049 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f940b4d-36e8-4ebb-a5ee-d01603181fca
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 35
    column: 5
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 978b67e1-81f6-406d-8d8a-203b24d78430
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 35
    column: 5
    function: main
  location_invariant:
    string: main__x <= 999949
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f528dcec-0ca6-4948-ae6e-0f61450f69e0
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 35
    column: 5
    function: main
  location_invariant:
    string: main__y <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50547f23-08d5-4dd9-be62-5b156b2a4690
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 35
    column: 5
    function: main
  location_invariant:
    string: 1049LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f3aacef-cdbe-4d84-8e22-af2bc33d9d86
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 35
    column: 5
    function: main
  location_invariant:
    string: 999949LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4862118d-c532-4386-8da2-3db20c574431
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 36
    column: 1
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7aba387-8303-43e0-b33a-3fa745c7827e
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 36
    column: 1
    function: main
  location_invariant:
    string: main__y <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4fd979b-c80f-4bee-a274-5644112f75cf
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 37
    column: 1
    function: main
  location_invariant:
    string: -998 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76fda251-2c7a-4db5-a5a0-1bf32e2b34c1
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 37
    column: 1
    function: main
  location_invariant:
    string: main__y <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ccee2bd4-9802-4ac7-b2ac-2dbfccb41747
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 39
    column: 1
    function: main
  loop_invariant:
    string: -998 <= main__y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bc96c79-75c5-40c1-9577-7b0ab06868e0
    creation_time: 2023-01-27T16:29:33Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gsv2008.c.i.v+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+lhb-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+lhb-reducer.c: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+lhb-reducer.c
    file_hash: 2f79720b54b4b9430b2efff386b59c4cac88edea0ef8f0ba223c5daccad25b87
    line: 39
    column: 1
    function: main
  loop_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
