- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad84cfbb-66d5-4b38-a356-63017d93ab28
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 36
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1cc68654-d444-4e6e-827b-20159cd43b2d
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 37
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cefc9e2c-0b66-439b-988e-fcceeb4ad3ea
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 39
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 156fd107-7360-4202-979d-bfd56ca88745
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 40
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2075fdec-eccd-41b6-96bc-cce5363d7497
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 45
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db19175b-0121-4d65-a767-51e136f0e695
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 46
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25fe5708-5eb3-4392-87fe-fcb3cf28495c
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 54
    column: 5
    function: main
  location_invariant:
    string: main__y <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 229ef4d5-4ccd-4db0-adb3-cf8d1af14620
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 54
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5069827-6a09-4a6a-80f7-a729c946656a
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 75
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c255e0af-109d-4517-9a4a-71e0d8fa6130
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 11
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c234483-452e-4f3b-ac7d-2ff07dc4ccfb
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 11
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 251c5c81-80ec-4184-9057-8469e4e4925f
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 11
    column: 14
    function: main
  location_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e75b1c70-d29c-4f77-95d9-d3a99ad1dcfc
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 11
    column: 14
    function: main
  location_invariant:
    string: (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14592d4f-a95a-4f6c-b6db-c98f9f1a5605
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 12
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 528f6dbb-79f8-4730-9107-c93e6450ab0e
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 12
    column: 14
    function: main
  location_invariant:
    string: (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8adfb5a6-42ae-486c-accd-690f81ae4270
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 15
    column: 1
    function: main
  location_invariant:
    string: main__y <= 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 294a2279-2465-40f9-96ac-7f1fb41fd513
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 15
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1f99526-7a0f-4b12-a97f-e93227adb140
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 15
    column: 1
    function: main
  location_invariant:
    string: (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1fd71c2-a8e9-4016-ad86-6c06f4c407bb
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 16
    column: 5
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9303804e-c336-48b9-80a0-029da410060a
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 18
    column: 6
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 275b05f7-9f0a-49d5-a2c3-692ce0c3b294
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 20
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0315d1e-25e4-4ed3-a4bf-dd5d4b2ed37c
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 21
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 788ce3ba-ca0e-4205-907c-e9699164b113
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 27
    column: 6
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb6f7660-cc32-41a3-9053-e3c119bb0524
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 29
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c499a021-a7cc-4b39-9784-b39d258751f9
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 30
    column: 1
    function: main
  location_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a4adb4b-7d78-4c86-99ca-fff8045352b3
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 15
    column: 1
    function: main
  loop_invariant:
    string: main__y <= 1U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3e988e1-9db3-4971-a56d-74da44187d50
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 15
    column: 1
    function: main
  loop_invariant:
    string: 1LL - (long long )main__y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d3de7d49-56c2-4f10-b5d2-63d673fd2d5f
    creation_time: 2023-01-27T16:29:43Z
    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/mod3.c.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/mod3.c.v+cfa-reducer.c
      input_file_hashes:
        ../plain/mod3.c.v+cfa-reducer.c: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mod3.c.v+cfa-reducer.c
    file_hash: 92b4501808affebdeca741bfd6f75263ab313d5eceb196bbb78aea107ecea6ed
    line: 15
    column: 1
    function: main
  loop_invariant:
    string: (long long )main__y >= 0LL
    type: assertion
    format: C
