- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e04cefe8-fbb9-4fe5-ace0-8d13600a2067
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 43
    column: 1
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 739c7e3e-60a2-44a0-acf1-fc62a0e9a86f
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 43
    column: 1
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9918f276-e3a8-4e13-bf48-8f54044ede39
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 43
    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: 97b56c3e-26dc-4164-aa20-3bfa773d0881
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 45
    column: 1
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e78562e-1b82-47ac-8b05-943921be3e24
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 45
    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: 4c65d4c5-02ca-465f-af1e-7a1df0c3bb74
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 46
    column: 5
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e4da5b8-48be-444c-a166-76660d568136
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 46
    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: 46760df0-3a07-4ec4-b700-203ddf86e289
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 48
    column: 2
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3037a3fc-42ae-41d7-bc36-906707744c9c
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 48
    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: dc2ce15d-b501-4c27-bac5-56ac7f3858bd
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 49
    column: 1
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 248cd704-f3ff-486c-ba99-e1c0f90af1f0
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 49
    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: 1e71ae3b-618e-48b8-a3e3-57717e843e57
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 53
    column: 2
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2511b8b2-ad47-4c6e-913a-bbc706600f7d
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 53
    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: 154ff8a7-59b6-49fc-bd82-9613056e0419
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 54
    column: 1
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 693f3c6e-5d7f-496d-8b63-e9cdaecd7a88
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    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: 6414a219-4863-4a06-a7bb-9555e614e2a3
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 21
    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: 9822e902-8fa1-424c-a811-7a8989a5776e
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 25
    column: 5
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 763e50c8-b96c-4797-8ac7-0436f1ad03b5
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 25
    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: 91cd6d14-4cbf-4991-83ae-67a81942b290
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 27
    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: 32b49b01-92a6-4370-9690-466f8a0a72a1
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 32
    column: 5
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d145c5bc-f43d-40a8-a322-d624e321266c
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 32
    column: 5
    function: main
  location_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3142c7c-07a2-4d8a-85e1-44d2b4a04ed7
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 32
    column: 5
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f914a6c7-8377-43ab-9572-f9b48ffec8e0
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    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: 977ffc2a-ec97-452e-89f4-2764ce644c6e
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 34
    column: 1
    function: main
  location_invariant:
    string: main__x <= -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1804833c-2724-48f6-87ce-5596b3d5ac32
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 34
    column: 1
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25d06bac-111b-4569-aff5-8f373f14d912
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 34
    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: f0b55bed-8d28-4ed1-b7af-d3e908eb0587
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 34
    column: 1
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb8ecbce-a3cd-4ed4-9618-1c1e6bea4123
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    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: b01510cc-ce12-4159-8d4b-7cea63a7c344
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 35
    column: 5
    function: main
  location_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4eae73a7-cbbb-46ba-b89a-ffe60d6a0a5f
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 35
    column: 5
    function: main
  location_invariant:
    string: (998051LL + (long long )main__x) + 998LL * (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b224228-9629-4eb7-9eb7-6a7259600e55
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 35
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )main__x) + (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c78ebd9-c4a9-4c65-a834-f18ed8b164ab
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 36
    column: 1
    function: main
  location_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96278b5a-bdfd-4675-b36f-6d9e64743ce0
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: -999 <= main__y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fa9bbf81-1243-466f-a416-c78da81af54b
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: caa2e1e0-01a8-49f6-9ac2-3ac419e139d2
    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+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/gsv2008.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/gsv2008.c.i.v+cfa-reducer.c: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gsv2008.c.i.v+cfa-reducer.c
    file_hash: 89dff477769dad0aa6457e2937a274d22cdfac537ecc3260d5e7568cec79996c
    line: 32
    column: 5
    function: main
  loop_invariant:
    string: (998051LL + (long long )main__x) + 999LL * (long long )main__y >= 0LL
    type: assertion
    format: C
