- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b329d84-cfcc-46b9-bde1-d4a5f558898c
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bb19933-0515-4822-9bf5-bf646a4e76fb
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f78d529f-df98-4902-8647-f51f1303a10d
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3431400-4572-4b90-9c4a-788cebe7122a
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0df6a92-24d0-4e64-91d1-e5b7442cadd4
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 742a8bd2-dade-482e-a2f3-ab1046cd6ab9
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc8bf52d-d3d9-44c9-b909-143f7d2fc7f9
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6ce4eb9-a892-4d34-90e8-605d9bd902c0
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62d43357-7ad7-44f9-b5e0-806c9a921d35
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 30
    column: 5
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9bd511b-d031-4a82-8807-37b09d6e5024
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 30
    column: 5
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c900b269-b4ab-4f22-8f69-8450a5680cf0
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae063103-fa57-4279-a6bc-b3e5e804afd2
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 086b2303-910a-4b5c-90c8-993c7462a678
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad874589-aee7-46ba-a4ef-8742fb63ffa8
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 32
    column: 1
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc032667-19a6-47f5-b1c4-4f80cc688bc4
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 32
    column: 1
    function: main
  location_invariant:
    string: 0 <= m
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f150946-e221-4f87-9ca1-172a4c635772
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 32
    column: 1
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c14ed48f-db90-44a8-a2a7-573caf51b05e
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 32
    column: 1
    function: main
  location_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d17b5ce5-d90a-4fd8-9b03-6cb339e3b6e2
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 32
    column: 1
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fa117bf-13b6-4e3f-ab79-6ba263735434
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 32
    column: 1
    function: main
  location_invariant:
    string: (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 224da20a-021d-446c-bc8f-68318a1a5730
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a866c9fa-d357-40ed-8f20-dd9562bed3f0
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )m - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67c5d285-c9b4-446b-ae4b-a6cb4680333c
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )m >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 027933d3-482c-45f9-bb97-448e905cea81
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8c915df-0c67-4939-8fa2-a40778ce64b2
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )n) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 606a3d19-50ff-4767-a303-3e9a74cf830c
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 28
    column: 10
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 33389a86-6648-42f7-95c6-6cf25bd1b34e
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 28
    column: 10
    function: main
  loop_invariant:
    string: 0 <= m
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c450bf1-48eb-4c83-ac75-6f166d40e1d4
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 28
    column: 10
    function: main
  loop_invariant:
    string: (0LL - (long long )m) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b3f86ec-a063-423e-9771-0c99faf779a5
    creation_time: 2023-01-27T16:29:32Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/gj2007b.i'''
    task:
      input_files:
      - ../plain/gj2007b.i
      input_file_hashes:
        ../plain/gj2007b.i: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gj2007b.i
    file_hash: a5dbdf40c5c8abdf745ea2973f48a7f1bd1d56b53cd410b7a2d364d83fc651a9
    line: 28
    column: 10
    function: main
  loop_invariant:
    string: (long long )m >= 0LL
    type: assertion
    format: C
