- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a04c9d7-b8c7-4ec1-b11a-d7f32f5a8aa6
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  location_invariant:
    string: 9 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd7adfcb-824c-41a9-9e88-8962d33e34b0
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  location_invariant:
    string: 50 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4411898e-840c-42af-b019-ef5aeb236871
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  location_invariant:
    string: main__x <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfb22635-5c98-4bd2-b891-a5c1eaaecc36
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45a2af62-2561-40ab-aced-ec5fc182ad98
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 74
    column: 5
    function: main
  location_invariant:
    string: 9 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6885639b-1243-47aa-96ec-c269fdbb2244
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 74
    column: 5
    function: main
  location_invariant:
    string: main__x <= 99
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54c929f3-955a-439e-be72-cedd412f33a3
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 74
    column: 5
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 708a90b9-53d3-48d6-8a1c-305822d48325
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 74
    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: b4b92e20-820d-4288-b1e7-66628ee0b1a4
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 76
    column: 1
    function: main
  location_invariant:
    string: 9 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44920866-ca99-42ed-9855-0e263665cdf3
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 76
    column: 1
    function: main
  location_invariant:
    string: 50 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58a8b44a-0cb0-47cd-b4bd-ea3694392da0
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 76
    column: 1
    function: main
  location_invariant:
    string: main__x <= 49
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 419d5a28-3e2b-4274-a92d-1a9f1c1deea3
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 76
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8be6427-4c76-4399-911e-e405460d0ff2
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 76
    column: 1
    function: main
  location_invariant:
    string: 49LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ab4d1f7-0e9d-4b70-896d-c21b0854bc93
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 82
    column: 1
    function: main
  location_invariant:
    string: 50 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ed818e4-15c7-4dee-aa13-b352d21539c5
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 82
    column: 1
    function: main
  location_invariant:
    string: main__x <= 99
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0747c4b6-b769-4b23-bfb8-86441791c6ce
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 82
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e79a9d8-baf7-4deb-8ef8-7247bba66fd8
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 82
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a694e2b-33b5-4aa9-80b0-f9486f49ddbf
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 82
    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: 6a2e5c9d-1238-48fa-ad68-a6de40b88d6b
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 82
    column: 1
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccab22c3-36df-4487-9df6-03e1fba2d8ac
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    column: 1
    function: main
  location_invariant:
    string: 50 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 052613ad-a2b2-42c5-b56b-d5104a182bc6
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    column: 1
    function: main
  location_invariant:
    string: 51 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c6d9d58-5374-478d-b075-54604cc071b7
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    column: 1
    function: main
  location_invariant:
    string: main__x <= 100
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 206c5157-b7d4-4d38-97e8-11791590335f
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    column: 1
    function: main
  location_invariant:
    string: -51LL + (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e9723b0-b5c4-46bc-bc51-99aaf6064861
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6874374c-3df9-4a11-b180-fa1971fa94d4
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    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: bb4318b6-c1e9-4fbe-9f4a-92ddc81918c1
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 83
    column: 1
    function: main
  location_invariant:
    string: main__x != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0f32cb0-dd7c-4ae9-b25a-39158366e718
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 91
    column: 1
    function: main
  location_invariant:
    string: 50 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e3f054a-2895-4244-854c-e7d730fbc924
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 91
    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: d420045e-9f06-4600-be68-ce8e575b3bd5
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 91
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 988dcee7-a95b-459c-841e-6b9492514762
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 93
    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: 1d0d6041-ab16-46d5-a733-fd0a7c9de11d
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 93
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6fad56f-e6ca-4395-852d-bfc894aa108f
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 94
    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: 8e2e2933-47a1-4845-9a53-d153a7f97a3a
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 94
    column: 5
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 148560a7-f6d9-4a7d-9910-a7a56177fa8f
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 96
    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: 19bca28f-d6c8-4300-82f1-9faf5ed5d4b8
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 96
    column: 2
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3492de1-cac7-4bf0-b729-569f8f651867
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 97
    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: 02a61ece-ce49-4ef2-95f5-a8a3fc16293d
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 97
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c111904b-d852-4b5f-a641-04afb025b3ad
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 101
    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: 58ce7ad9-56be-4679-9e93-881784cc2bcc
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 101
    column: 2
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 545b2071-2467-49c6-a95e-a8046802d136
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 102
    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: 921d3cfe-65fe-452d-b8f5-339183f101c1
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 102
    column: 1
    function: main
  location_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eec5f8fd-f443-47a7-b3fe-c40ba6f389ad
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  loop_invariant:
    string: 9 <= main__x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c661ea78-8ce9-4f65-a4fc-08b38a53be8b
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  loop_invariant:
    string: 50 <= main__y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c56b5200-5931-4193-962b-24afe8fd2deb
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  loop_invariant:
    string: main__x <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0321a0a-c554-4f4a-8067-6537f5ff0314
    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+lhb-reducer.c'''
    task:
      input_files:
      - ../plain/gj2007.c.i.p+lhb-reducer.c
      input_file_hashes:
        ../plain/gj2007.c.i.p+lhb-reducer.c: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007.c.i.p+lhb-reducer.c
    file_hash: 1ae3736aabcb020d122100864e41791456e1f94490735ab1a93eef5c54883fe7
    line: 72
    column: 5
    function: main
  loop_invariant:
    string: -50LL + (long long )main__y >= 0LL
    type: assertion
    format: C
