- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9630e12e-0b0c-4314-b8b7-47c5b0db5332
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 19
    column: 8
    function: lcp
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95b10903-d5ab-4a24-aa0a-16d7ed67b1a4
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 19
    column: 8
    function: lcp
  location_invariant:
    string: ((-1LL - (long long )l) + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d288456-5258-4976-8d62-56b14c882548
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 19
    column: 8
    function: lcp
  location_invariant:
    string: ((-1LL - (long long )l) + (long long )n) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82d47407-afb4-4741-9fcc-94d0c4378e89
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 19
    column: 8
    function: lcp
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6411769-202e-4060-85c6-d35383c15b9f
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 21
    column: 4
    function: lcp
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06050a2b-ddfb-4f44-9f22-c38b8a353f47
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 21
    column: 4
    function: lcp
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88fb35ea-df7e-48a0-b97c-2545e4d6ba79
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 26
    column: 8
    function: check
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2db1956a-b7ef-44c4-8a14-64e95e6da0c1
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 27
    column: 4
    function: check
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fab6bfe2-18d0-4953-ad3f-203a76a825b8
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 27
    column: 4
    function: check
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf981e44-004b-4137-955f-cd823f71abdf
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 27
    column: 4
    function: check
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76863723-31b7-479a-b179-9a1898ccb8b3
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 27
    column: 4
    function: check
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbcf7645-1016-4f33-9894-4305d39ee9bc
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 31
    column: 7
    function: check
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5f8a696-d0e1-451b-b2ea-94736a8d0489
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 31
    column: 7
    function: check
  location_invariant:
    string: -2147483647 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19a28577-03ee-4dda-8219-467161ec28a7
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 31
    column: 7
    function: check
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a96c2fe-6574-4b30-a9e5-64260458c0ff
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 31
    column: 7
    function: check
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18fa0130-b94c-47a6-97c6-1e7be28ec4de
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 31
    column: 7
    function: check
  location_invariant:
    string: ((-1LL - (long long )l) + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3e4249a-6333-4d6e-9753-7a1e04d03ddf
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 32
    column: 8
    function: check
  location_invariant:
    string: -2147483647 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4daffec9-aff5-4901-b88d-3b90781ac44c
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 32
    column: 8
    function: check
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 186ee535-b096-4f57-a0e5-451349021c2c
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 32
    column: 8
    function: check
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f73f01ff-ba55-49bc-ab42-0efe8fee9319
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 32
    column: 8
    function: check
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec3fc486-960d-453b-b1c5-41b224d6d2e3
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 32
    column: 8
    function: check
  location_invariant:
    string: ((-1LL - (long long )l) + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3886bd50-2bb9-41b2-9832-e7c55eeb3196
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 32
    column: 8
    function: check
  location_invariant:
    string: ((-1LL - (long long )l) + (long long )n) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fae7d0d-f53a-4ad9-95f7-767f261913c1
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 38
    column: 4
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05d810e9-7fe0-4dcb-9c99-8a74f7c89301
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 38
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2ee2581-71d3-4b10-91ca-dcc7463236f0
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 45
    column: 4
    function: main
  location_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57c29dea-a575-4d23-82a0-bafb4666c48f
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 45
    column: 4
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a813d90f-f910-4633-ac5d-2cb4a7d09003
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 47
    column: 4
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78c897bc-e9f0-47b5-a97e-33c836b7043e
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7745566c-5e73-402a-a282-766d70915c73
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 18
    column: 11
    function: lcp
  loop_invariant:
    string: 0 <= l
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 192f0537-88a7-4e30-8e65-26e4e28c8a23
    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/lcp.c'''
    task:
      input_files:
      - ../plain/lcp.c
      input_file_hashes:
        ../plain/lcp.c: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcp.c
    file_hash: 1e47fbc54bff4eeebe072cdb8acf7cfe734a91f148fd421ae1769ba3b81a6f5a
    line: 18
    column: 11
    function: lcp
  loop_invariant:
    string: (long long )l >= 0LL
    type: assertion
    format: C
