- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: faeea5f2-37fd-4db9-87c4-576c24d118ed
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 37
    column: 1
    function: main
  location_invariant:
    string: 1 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d44ebdac-8dd5-4977-90c7-b9216920b979
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 37
    column: 1
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c99dab94-82bf-48f4-81c1-094b67ba8f9b
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 37
    column: 1
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98c4dc1e-aed6-4c15-9ca7-79b885ea544a
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 38
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e05c6a62-8d86-4957-bc11-2d3824f9c0e1
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 38
    column: 5
    function: main
  location_invariant:
    string: main__x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 958e881d-ffd8-4ca1-a918-696f64fd6dbe
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 38
    column: 5
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6eecb1e1-0d18-410b-9344-97d5fd8b77e3
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 38
    column: 5
    function: main
  location_invariant:
    string: main__x != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44a10334-75e7-465a-b6cd-96e786278f5e
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 39
    column: 1
    function: main
  location_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 174fceb6-f920-4706-8a4d-e884efd1a144
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 44
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5d9f58b-aa0e-43f8-b8a6-c7c9f28696d3
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 44
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0245e66-16e9-491f-a64e-e5787efbc702
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 44
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: add0e679-c685-45d7-b4c3-301e3d3a7c51
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 44
    column: 5
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 360dd426-7a87-4060-a1d5-d12fadb77f77
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 48
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 518170dc-23c3-4328-8737-f1a534516c22
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 50
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28234f27-fda4-48d1-83a0-9ac5d2d2d839
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 51
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91a1b973-677c-4fd4-afbb-3b1dcbc0a8d4
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 58
    column: 2
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c62f7cb-2337-491b-b32f-5289b2e2f43c
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 59
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44ef7496-defe-4e7b-a90a-1db3c1bc8c20
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 65
    column: 1
    function: main
  location_invariant:
    string: (-1LL + (long long )main__i) + (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5f2086d-82bb-4567-8747-1e505cf9b50b
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 65
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89c6b1f6-7a91-40df-be70-abb826c34b79
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 65
    column: 1
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53fc4eba-cd5d-480b-91a4-6c9693214aa6
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 21
    column: 1
    function: main
  location_invariant:
    string: -1LL - (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b65e24f3-b7a2-497f-86b5-61513a37f5cd
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 25
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63a5ae8f-287d-4398-9de7-67336c8cf003
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 27
    column: 1
    function: main
  location_invariant:
    string: -1LL - (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d4ae672-69fc-4506-a0b4-d09cb7d41639
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 27
    column: 1
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9a16f8a-16cc-4498-adb9-ac257c6fbd7e
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 31
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d72e79b4-c356-4ec6-841b-2ca8437e8560
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d11a5acf-63cb-487d-b789-990f6f2d3a68
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64083995-825b-41f5-ace6-f41068443477
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 32
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bbdf8ec-83ad-45fe-8c32-9a48a924c68c
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 32
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdf6f0ac-cca1-43d6-bdb0-1a5e10ca49c3
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 32
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9ff51df-1c01-4a4a-8387-7738e06f6ef5
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 32
    column: 5
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 047ba195-fcd6-4db7-9f67-c35eaf4df2e9
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  location_invariant:
    string: 0 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27bfadc0-d2fc-4e4b-8f19-2dc9c3d0fb3c
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a0d9802-31b6-412b-ae6a-c3285381f36b
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fc12fb3-26f5-4d02-a638-7e9dea6e5ee2
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    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: ab2efb45-0dbd-4d3a-a186-4e102d8a158f
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 36
    column: 5
    function: main
  location_invariant:
    string: 1 <= main__x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ef2775c-c3a8-44a3-9e38-2deecaf5c340
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 36
    column: 5
    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: 39106acf-de6c-46fb-8585-70c4d6f07e17
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 36
    column: 5
    function: main
  location_invariant:
    string: (long long )main__i - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55f2f8c4-4109-47a3-9bb9-f1578171ea3a
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 36
    column: 5
    function: main
  location_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bfaa988-9145-42fa-be63-508513e8eedf
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 36
    column: 5
    function: main
  location_invariant:
    string: main__x != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 94621d14-8ed1-4b7b-8bd7-0f484848efad
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: 0 <= main__i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 10e2167d-4bfc-4390-8194-347166be7c22
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: 0 <= main__j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f0abeb1-ee4e-4a14-a42b-6cf1e77aecb4
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: 0 <= main__x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e8ffa610-e366-481b-95f8-99cb4941a413
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )main__i - (long long )main__x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0225cf6f-23af-4800-85ac-cce10c733aed
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )main__j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2dfc49f0-209f-4d99-a8c9-c38e4ebfd1f5
    creation_time: 2023-01-27T16:29:40Z
    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/jm2006.c.i.v+cfa-reducer.c'''
    task:
      input_files:
      - ../plain/jm2006.c.i.v+cfa-reducer.c
      input_file_hashes:
        ../plain/jm2006.c.i.v+cfa-reducer.c: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/jm2006.c.i.v+cfa-reducer.c
    file_hash: d85bf43cff1a30e10d1e3bbf4675032df62c31f758d5324913387f5dfb870a68
    line: 34
    column: 5
    function: main
  loop_invariant:
    string: (long long )main__x >= 0LL
    type: assertion
    format: C
